Theorem Algebra.FormallySmooth.iff_injective_and_projective

Modification history

2025-11-06 18:48
Mathlib/RingTheory/Smooth/Kaehler.lean
chore(RingTheory): redefine `FormallySmooth` in terms of `Ω[S⁄R]` and `H¹(L_{S/R})` (#30876) …
Deleted Algebra.FormallySmooth.iff_injective_and_projectiveView on Github →
2024-11-02 12:25
Mathlib/RingTheory/Smooth/Kaehler.lean
feat(RingTheory/Smooth): formally smooth iff `H¹(L_{R/S}) = 0` and `Ω_{S/R}` is projective (#17905)
Added Algebra.FormallySmooth.iff_injective_and_projectiveView on Github →