Commit 2026-02-06 15:35 12e4f5a9

View on Github →

feat(RingTheory): local structure of monogenic unramified algebras (#33903)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean

added theorem Ideal.exists_mem_span_singleton_map_residueField_eq

added theorem Polynomial.fiberEquivQuotient_tmul

Modified Mathlib/RingTheory/Localization/AtPrime/Basic.lean

added theorem Localization.localAlgHom_apply

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

added theorem Algebra.TensorProduct.adjoin_one_tmul_image_eq_top

Modified Mathlib/RingTheory/Unramified/Field.lean

added theorem Algebra.IsUnramifiedAt.not_minpoly_sq_dvd

Created Mathlib/RingTheory/Unramified/LocalStructure.lean

added theorem Algebra.IsUnramifiedAt.exists_hasStandardEtaleSurjectionOn_of_exists_adjoin_singleton_eq_top

added theorem HasStandardEtaleSurjectionOn.isStandardEtale

added theorem HasStandardEtaleSurjectionOn.mk

added theorem HasStandardEtaleSurjectionOn.of_dvd

added def HasStandardEtaleSurjectionOn

Modified Mathlib/RingTheory/Unramified/Locus.lean

added theorem Algebra.IsUnramifiedAt.residueField