Commit 2026-02-09 13:22 383aca4b

View on Github →

refactor: move Polynomial.toSubring to a new file (#34661) This aids discoverability, which I think is a good thing given that this has been reinvented at least thrice! Twice in Mathlib (Polynomial.toSubring, Polynomial.int), plus once by myself in the CGT repo (Nimber.IsField.embed).

Estimated changes

Modified Mathlib.lean

Modified Mathlib/FieldTheory/Fixed.lean

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/RingTheory/Algebraic/Integral.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

deleted theorem Polynomial.coeff_ofSubring

deleted theorem Polynomial.coeff_toSubring'

deleted theorem Polynomial.coeff_toSubring

deleted theorem Polynomial.coeffs_ofSubring

deleted theorem Polynomial.degree_toSubring

deleted theorem Polynomial.map_toSubring

deleted theorem Polynomial.monic_toSubring

deleted theorem Polynomial.natDegree_toSubring

deleted def Polynomial.ofSubring

deleted theorem Polynomial.support_toSubring

deleted def Polynomial.toSubring

deleted theorem Polynomial.toSubring_one

deleted theorem Polynomial.toSubring_zero

Created Mathlib/RingTheory/Polynomial/Subring.lean

added theorem Polynomial.coeff_ofSubring

added theorem Polynomial.coeff_toSubring'

added theorem Polynomial.coeff_toSubring

added theorem Polynomial.coeffs_ofSubring

added theorem Polynomial.degree_toSubring

added theorem Polynomial.map_toSubring

added theorem Polynomial.monic_toSubring

added theorem Polynomial.natDegree_toSubring

added theorem Polynomial.support_toSubring

added theorem Polynomial.toSubring_one

added theorem Polynomial.toSubring_zero