Theorem Algebra.IsStandardSmoothOfRelativeDimension.of_algEquiv

Modification history

2025-12-21 17:00

Mathlib/RingTheory/Smooth/StandardSmooth.lean

feat(RingTheory/Smooth/StandardSmooth): transport `IsStandardSmooth` along algebra isomorphisms (#32925)

Added Algebra.IsStandardSmoothOfRelativeDimension.of_algEquiv View on Github →