Commit 2025-12-21 17:00 da22c4ea

View on Github →

feat(RingTheory/Smooth/StandardSmooth): transport IsStandardSmooth along algebra isomorphisms (#32925)

Estimated changes

Modified Mathlib/RingTheory/Extension/Generators.lean

added theorem Algebra.Generators.ker_ofAlgEquiv

added def Algebra.Generators.ofAlgEquiv

added theorem Algebra.Generators.ofAlgEquiv_val

Modified Mathlib/RingTheory/Extension/Presentation/Basic.lean

added theorem Algebra.Presentation.dimension_ofAlgEquiv

added def Algebra.Presentation.ofAlgEquiv

Modified Mathlib/RingTheory/Extension/Presentation/Submersive.lean

added theorem Algebra.PreSubmersivePresentation.jacobiMatrix_ofAlgEquiv

added theorem Algebra.PreSubmersivePresentation.jacobian_ofAlgEquiv

added def Algebra.PreSubmersivePresentation.ofAlgEquiv

added def Algebra.SubmersivePresentation.ofAlgEquiv

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

added theorem Algebra.IsStandardSmooth.of_algEquiv

added theorem Algebra.IsStandardSmoothOfRelativeDimension.of_algEquiv