Theorem Algebra.Extension.tensorCotangentSpace_tmul_tmul

Modification history

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