Theorem Matrix.toLpLin_symm_id

Modification history

2026-01-27 22:28
Mathlib/Analysis/Normed/Lp/Matrix.lean
refactor: Generalize Matrix.toEuclideanLin to PiLp (#34241) …
Added Matrix.toLpLin_symm_idView on Github →