Theorem Algebra.Extension.CotangentSpace.map_tmul_eq_tmul_map

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.CotangentSpace.map_tmul_eq_tmul_mapView on Github →