Theorem TensorProduct.map_convMul_map

Modification history

2025-11-04 14:52
Mathlib/RingTheory/Coalgebra/Convolution.lean
feat(RingTheory/Coalgebra/Convolution): `(f ⊗ₘ g) * (h ⊗ₘ k) = (f * h) ⊗ₘ (g * k)` (#31251)
Added TensorProduct.map_convMul_mapView on Github →