Theorem RingHom.IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAway

Modification history

2024-10-16 11:05
Mathlib/RingTheory/RingHom/StandardSmooth.lean
feat(RingTheory/StandardSmooth): meta properties of standard smooth ring homomorphisms (#16868) …
Added RingHom.IsStandardSmoothOfRelativeDimension.algebraMap_isLocalizationAwayView on Github →