Theorem RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero

Modification history

2026-02-10 11:38
Mathlib/RingTheory/RingHom/LocallyStandardSmooth.lean
refactor(AlgebraicGeometry/Smooth): replace `Locally IsStandardSmooth` by `Smooth` (#35034) …
Added RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zeroView on Github →