Theorem RingHom.IsStandardSmooth.toAlgebra

Modification history

2025-04-03 10:34

Mathlib/RingTheory/RingHom/StandardSmooth.lean

refactor(RingTheory/Smooth): remove universe parameters for generators and relations in `Algebra.IsStandardSmooth` (#23553) …

Modified RingHom.IsStandardSmooth.toAlgebra View on Github →

2024-10-17 11:36

Mathlib/RingTheory/RingHom/StandardSmooth.lean

feat(Algebraize): Fix algebraize tactic (#17839) …

Added RingHom.IsStandardSmooth.toAlgebra View on Github →