Theorem Irreducible.exists_dvd_monic_irreducible_of_isIntegral

Modification history

2024-01-08 14:36
Mathlib/RingTheory/AdjoinRoot.lean
feat(FieldTheory/IsSepClosed): add some results on separable closure and perfect field (#9522) …
Added Irreducible.exists_dvd_monic_irreducible_of_isIntegralView on Github →