Theorem Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijective

Modification history

2024-09-17 21:38
Mathlib/RingTheory/Smooth/StandardSmooth.lean
feat(RingTheory/StandardSmooth): ring isomorphisms are standard smooth (#16869) …
Added Algebra.IsStandardSmoothOfRelativeDimension.of_algebraMap_bijectiveView on Github →