Commit 2023-06-16 06:56 8586e8c4

View on Github →

feat: port FieldTheory.Minpoly.IsIntegrallyClosed (#5076)

depends on: #5069

Estimated changes

Modified Mathlib.lean

Created Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean

added def minpoly.Algebra.adjoin.powerBasis'

added theorem minpoly.IsIntegrallyClosed.Minpoly.unique

added theorem minpoly.IsIntegrallyClosed.degree_le_of_ne_zero

added theorem minpoly.ToAdjoin.injective

added def minpoly.equivAdjoin

added theorem minpoly.isIntegrallyClosed_dvd

added theorem minpoly.isIntegrallyClosed_dvd_iff

added theorem minpoly.isIntegrallyClosed_eq_field_fractions'

added theorem minpoly.isIntegrallyClosed_eq_field_fractions

added theorem minpoly.ker_eval

added theorem minpoly.prime_of_isIntegrallyClosed