feat(ring_theory/discriminant): remove an assumption (#11359)
feat(ring_theory/discriminant): remove an assumption (#11359)

We remove a `nonempty` assumption.





leanprover-community/mathlib,leanprover-community/mathlib