Theorem RingHom.IsStandardSmoothOfRelativeDimension.toAlgebra

Modification history

2024-10-17 11:36
Mathlib/RingTheory/RingHom/StandardSmooth.lean
feat(Algebraize): Fix algebraize tactic (#17839) …
Added RingHom.IsStandardSmoothOfRelativeDimension.toAlgebraView on Github →