Theorem RingHom.Smooth.comp

Modification history

2025-11-06 18:48
Mathlib/RingTheory/RingHom/Smooth.lean
chore(RingTheory): redefine `FormallySmooth` in terms of `Ω[S⁄R]` and `H¹(L_{S/R})` (#30876) …
Modified RingHom.Smooth.compView on Github →
2025-05-28 12:51
Mathlib/RingTheory/RingHom/Smooth.lean
feat(RingHom): define `RingHom.Smooth` (#25107)
Added RingHom.Smooth.compView on Github →