Theorem Matrix.instCstarRing

Modification history

2024-08-06 04:16

Mathlib/Analysis/CStarAlgebra/Matrix.lean

chore(*): rename `Cstar*` to `CStar*` (#15495) …

Deleted Matrix.instCstarRing View on Github →

2024-01-09 14:39

Mathlib/Analysis/NormedSpace/Star/Matrix.lean

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

Added Matrix.instCstarRing View on Github →