Theorem commute_mulLeftLinearMap_mulRightLinearMap

Modification history

2024-12-20 05:45
Mathlib/Data/Matrix/Bilinear.lean
feat: add bundled multiplication maps for matrices (#19229) …
Added commute_mulLeftLinearMap_mulRightLinearMapView on Github →