Commit 2024-11-02 12:25 773f9ce4

View on Github →

feat(RingTheory/Smooth): formally smooth iff H¹(L_{R/S}) = 0 and Ω_{S/R} is projective (#17905)

Estimated changes

Modified Mathlib/RingTheory/Smooth/Kaehler.lean

added theorem Algebra.FormallySmooth.iff_injective_and_projective

added theorem Algebra.FormallySmooth.iff_injective_and_split

added theorem Algebra.FormallySmooth.iff_split_injection

added theorem Algebra.FormallySmooth.iff_subsingleton_and_projective

added def derivationQuotKerSq

added theorem derivationQuotKerSq_mk

added def retractionKerCotangentToTensorEquivSection

added def tensorKaehlerQuotKerSqEquiv

added theorem tensorKaehlerQuotKerSqEquiv_symm_tmul_D

added theorem tensorKaehlerQuotKerSqEquiv_tmul_D

Modified scripts/noshake.json