[Merged by Bors] - feat(RingTheory/Smooth): calculate `H¹(L)` via formally smooth extensions#20471

Closed

erdOne wants to merge 5 commits intomasterfrom erd1/equivH1Cotangent

+159-18

Commits on Jan 4, 2025

feat(RingTheory/Smooth): calculate H¹(L) via formally smooth extensions
erdOne
committed

Commits on Jan 6, 2025

Commits on Jan 8, 2025

Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into erd1/equivH1Cotangent
erdOne
committed