Theorem TensorProduct.intrinsicStar_map

Modification history

2026-02-10 22:14
Mathlib/Algebra/Star/LinearMap.lean
refactor: add type synonym for convolutive product of linear maps and intrinsic star (#34945) …
Modified TensorProduct.intrinsicStar_mapView on Github →
2025-10-31 17:31
Mathlib/Algebra/Star/LinearMap.lean
feat(Algebra/Star/LinearMap): `star mul' = mul' ∘ TensorProduct.comm` and `star (f ⊗ₘ g) = star f ⊗ₘ star g` (#31003)
Added TensorProduct.intrinsicStar_mapView on Github →