Commit 2025-03-26 19:05 7425f429

View on Github →

chore(RingTheory): erw cleanup from A to LocalRing (#23343) Get rid of almost all erws in these files. A few small _def lemmas added, otherwise mostly proof refactoring.

Estimated changes

Modified Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean

added theorem AdicCompletion.coe_ofTensorProductEquivOfFiniteNoetherian

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

Modified Mathlib/RingTheory/ClassGroup.lean

added theorem ClassGroup.mk_def

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

Modified Mathlib/RingTheory/DedekindDomain/Ideal.lean

Modified Mathlib/RingTheory/DedekindDomain/PID.lean

Modified Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean

Modified Mathlib/RingTheory/DiscreteValuationRing/Basic.lean

Modified Mathlib/RingTheory/Filtration.lean

Modified Mathlib/RingTheory/FinitePresentation.lean

Modified Mathlib/RingTheory/FiniteType.lean

Modified Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean

Modified Mathlib/RingTheory/FreeCommRing.lean

Modified Mathlib/RingTheory/Generators.lean

added theorem Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply

Modified Mathlib/RingTheory/Henselian.lean

Modified Mathlib/RingTheory/Ideal/IsPrincipal.lean

Modified Mathlib/RingTheory/Jacobson/Ideal.lean

Modified Mathlib/RingTheory/Jacobson/Ring.lean

Modified Mathlib/RingTheory/Kaehler/TensorProduct.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

added theorem LaurentSeries.valuation_def

Modified Mathlib/RingTheory/LocalRing/MaximalIdeal/Basic.lean

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

added theorem IsLocalRing.residue_def

Modified Mathlib/RingTheory/Valuation/ExtendToLocalization.lean

added theorem Valuation.extendToLocalization_mk'