Commit 2024-10-17 13:07 a0d31266

View on Github →

feat(RingTheory/Kaehler): the first homology of the cotangent complex (#17559)

Estimated changes

Modified Mathlib/RingTheory/Kaehler/CotangentComplex.lean

added def Algebra.Generators.H1Cotangent.equiv

added def Algebra.Generators.H1Cotangent.map

added theorem Algebra.Generators.H1Cotangent.map_comp

added theorem Algebra.Generators.H1Cotangent.map_eq

added theorem Algebra.Generators.H1Cotangent.map_id

added theorem Algebra.Generators.H1Cotangent.val_add

added theorem Algebra.Generators.H1Cotangent.val_smul

added theorem Algebra.Generators.H1Cotangent.val_zero

added def Algebra.Generators.H1Cotangent

added def Algebra.Generators.h1Cotangentι

added theorem Algebra.Generators.h1Cotangentι_ext

added theorem Algebra.Generators.h1Cotangentι_injective

added theorem Algebra.Generators.subsingleton_h1Cotangent

added def Algebra.H1Cotangent.map