Def Matrix.toEuclideanLin

Modification history

2026-01-27 22:28
Mathlib/Analysis/InnerProductSpace/PiL2.lean
refactor: Generalize Matrix.toEuclideanLin to PiLp (#34241) …
Deleted Matrix.toEuclideanLinView on Github →
2023-05-29 05:29
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat: port Analysis.InnerProductSpace.PiL2 (#4420) …
Added Matrix.toEuclideanLinView on Github →