Theorem RingHom.isStandardSmoothOfRelativeDimension_stableUnderBaseChange

Modification history

2024-11-06 16:11

Mathlib/RingTheory/RingHom/StandardSmooth.lean

refactor(CategoryTheory/MorphismProperty): turn `StableUnderBaseChange` into a class (#18692) …

Deleted RingHom.isStandardSmoothOfRelativeDimension_stableUnderBaseChange View on Github →

2024-10-16 11:05

Mathlib/RingTheory/RingHom/StandardSmooth.lean

feat(RingTheory/StandardSmooth): meta properties of standard smooth ring homomorphisms (#16868) …

Added RingHom.isStandardSmoothOfRelativeDimension_stableUnderBaseChange View on Github →