Theorem Algebra.Extension.exact_hCotangentι_cotangentComplex

Modification history

2026-03-17 15:35
Mathlib/RingTheory/Extension/Cotangent/Basic.lean
feat(RingTheory): `Extension.CotangentSpace` commutes with base change (#35594) …
Added Algebra.Extension.exact_hCotangentι_cotangentComplexView on Github →