Theorem LinearMap.det_mulLeft

Modification history

2024-12-20 14:57
Mathlib/LinearAlgebra/Determinant.lean
feat: determinant of left multiplication (#19873) …
Added LinearMap.det_mulLeftView on Github →