Commit 2025-07-03 03:52 7c5f1ba4

View on Github →

feat(RingTheory/Presentation): naive presentations of quotients (#26650)

Estimated changes

Modified Mathlib/RingTheory/Extension/Generators.lean

added theorem Algebra.Generators.ker_naive

added def Algebra.Generators.naive

added theorem Algebra.Generators.naive_σ

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

added def Algebra.Presentation.naive

added theorem Algebra.Presentation.naive_relation

added theorem Algebra.Presentation.naive_relation_apply

Modified Mathlib/RingTheory/Smooth/StandardSmooth.lean

added theorem Algebra.PreSubmersivePresentation.jacobiMatrix_naive

added def Algebra.PreSubmersivePresentation.naive