Commit 2026-03-17 15:35 42da4bc0

View on Github →

feat(RingTheory): Extension.CotangentSpace commutes with base change (#35594) From Pi1.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RingTheory/Extension/Basic.lean

Created Mathlib/RingTheory/Extension/Cotangent/BaseChange.lean

added def Algebra.Extension.tensorCotangentSpace

added theorem Algebra.Extension.tensorCotangentSpace_tmul

added theorem Algebra.Extension.tensorCotangentSpace_tmul_tmul

Modified Mathlib/RingTheory/Extension/Cotangent/Basic.lean

added theorem Algebra.Extension.CotangentSpace.map_tmul_eq_tmul_map

added theorem Algebra.Extension.exact_hCotangentι_cotangentComplex