Def Algebra.Generators.H1Cotangent.equiv

Modification history

2024-11-15 10:09

Mathlib/RingTheory/Kaehler/CotangentComplex.lean

refactor(RingTheory): generalize cotangent complex for arbitrary extensions (#18684)

Modified Algebra.Generators.H1Cotangent.equiv View on Github →

2024-10-17 13:07

Mathlib/RingTheory/Kaehler/CotangentComplex.lean

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

Added Algebra.Generators.H1Cotangent.equiv View on Github →