Def Matrix.toEuclideanClm

Modification history

2024-01-26 03:03

Mathlib/Analysis/NormedSpace/Star/Matrix.lean

fix: `Clm` -> `CLM`, `Cle` -> `CLE` (#10018) …

Deleted Matrix.toEuclideanClm View on Github →

2024-01-09 14:39

Mathlib/Analysis/NormedSpace/Star/Matrix.lean

feat: provide the ℓ² operator norm on matrices (#9474) …

Added Matrix.toEuclideanClm View on Github →