Theorem Algebra.FormallySmooth.iff_injective_and_split

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_split View 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_split View on Github →