Theorem Algebra.SubmersivePresentation.isStandardSmoothOfRelativeDimension

Modification history

2025-06-02 12:17
Mathlib/RingTheory/Smooth/StandardSmooth.lean
refactor(RingTheory): unbundle `rels` and `vars` from `Algebra.Presentation` (#25085)
Modified Algebra.SubmersivePresentation.isStandardSmoothOfRelativeDimensionView on Github →
2025-04-03 10:34
Mathlib/RingTheory/Smooth/StandardSmooth.lean
refactor(RingTheory/Smooth): remove universe parameters for generators and relations in `Algebra.IsStandardSmooth` (#23553) …
Added Algebra.SubmersivePresentation.isStandardSmoothOfRelativeDimensionView on Github →