mathlib3
8910f6d9 - feat(ring_theory/discriminant): remove an assumption (#11359)

Commit

4 years ago

feat(ring_theory/discriminant): remove an assumption (#11359) We remove a `nonempty` assumption.

Author

riccardobrasca

Parents