Def Algebra.Extension.H1Cotangent.equiv

Modification history

2025-01-08 16:06

Mathlib/RingTheory/Kaehler/CotangentComplex.lean

feat(RingTheory/Smooth): calculate `H¹(L)` via formally smooth extensions (#20471)

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