Mathlib Changelog
v4
Changelog
About
Github
Theorem
Algebra.Extension.H1Cotangent.map_toInfinitesimal_bijective
Modification history
2025-01-08 16:06
Mathlib/RingTheory/Smooth/Kaehler.lean
feat(RingTheory/Smooth): calculate `H¹(L)` via formally smooth extensions (#20471)
Added
Algebra.Extension.H1Cotangent.map_toInfinitesimal_bijective
View on Github →