Commit 2022-06-29 20:38 71985dc5

View on Github →

feat(field_theory/minpoly): generalize statements about GCD domains (#14979) Currently, the statements about the minimal polynomial over a GCD domain R require the element to be in a K-algebra, where K is the fraction field of R. We remove this assumption. From flt-regular.

Estimated changes

Modified src/field_theory/minpoly.lean

added theorem minpoly.gcd_domain_degree_le_of_ne_zero

modified theorem minpoly.gcd_domain_dvd

added theorem minpoly.gcd_domain_eq_field_fractions'

modified theorem minpoly.gcd_domain_eq_field_fractions

added theorem minpoly.gcd_domain_unique

Modified src/number_theory/cyclotomic/discriminant.lean

Modified src/number_theory/cyclotomic/rat.lean

Modified src/ring_theory/polynomial/content.lean

added theorem polynomial.aeval_prim_part_eq_zero

added theorem polynomial.eval₂_prim_part_eq_zero

Modified src/ring_theory/polynomial/cyclotomic/basic.lean

Modified src/ring_theory/polynomial/eisenstein.lean

Modified src/ring_theory/roots_of_unity.lean