mathlib
3e7efd4e - feat(field_theory/separable): Remove hypothesis in irreducible.separable (#5687)

Commit

5 years ago

feat(field_theory/separable): Remove hypothesis in irreducible.separable (#5687) An irreducible polynomial is nonzero, so this hypothesis is unnecessary.

Author

tb65536

Parents

b72811f2

mathlib 3e7efd4e - feat(field_theory/separable): Remove hypothesis in irreducible.separable (#5687)

mathlib
3e7efd4e - feat(field_theory/separable): Remove hypothesis in irreducible.separable (#5687)