Commit 2025-03-28 16:45 718d4fea

View on Github →

chore(RingTheory): even more erws (#23404) Nothing very exciting, just a few manual unfolds and a few erws removed through proof refactoring.

Estimated changes

Modified Mathlib/RingTheory/Presentation.lean

added theorem Algebra.Presentation.baseChange_toGenerators

added theorem Algebra.Presentation.toGenerators_comp

Modified Mathlib/RingTheory/RingHom/FinitePresentation.lean

Modified Mathlib/RingTheory/SimpleModule/Basic.lean

Modified Mathlib/RingTheory/Smooth/Basic.lean

Modified Mathlib/RingTheory/Smooth/Kaehler.lean

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

added theorem Algebra.PreSubmersivePresentation.baseChange_ring

added theorem Algebra.PreSubmersivePresentation.baseChange_toPresentation

added theorem Algebra.PreSubmersivePresentation.toGenerators_comp

added theorem Algebra.PreSubmersivePresentation.toPresentation_comp

Modified Mathlib/RingTheory/TensorProduct/MvPolynomial.lean

Modified Mathlib/RingTheory/Valuation/ValuationRing.lean

Modified Mathlib/RingTheory/Valuation/ValuationSubring.lean

Modified Mathlib/RingTheory/WittVector/Isocrystal.lean