Theorem mulRightLinearMap_zero_eq_zero

Modification history

2025-07-25 22:49
Mathlib/Data/Matrix/Bilinear.lean
chore: fix more indentation (#27494) …
Modified mulRightLinearMap_zero_eq_zeroView on Github →
2024-12-20 05:45
Mathlib/Data/Matrix/Bilinear.lean
feat: add bundled multiplication maps for matrices (#19229) …
Added mulRightLinearMap_zero_eq_zeroView on Github →