Theorem tensorKaehlerQuotKerSqEquiv_symm_tmul_D

Modification history

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 tensorKaehlerQuotKerSqEquiv_symm_tmul_DView on Github →