Theorem LinearMap.det_toLpLin

Modification history

2026-03-18 15:17
Mathlib/Analysis/Normed/Lp/Matrix.lean
feat(Analysis/Lp): simp lemma for LinearMap.det and toLpLin (#36661) …
Added LinearMap.det_toLpLinView on Github →