Commit 2025-02-15 10:28 29b1fb72

View on Github →

chore(CStarMatrix): drop unneeded DecidableEq assumptions (#21894) Found by the linters in #10235

Estimated changes

Modified Mathlib/Analysis/CStarAlgebra/CStarMatrix.lean

modified theorem CStarMatrix.norm_entry_le_norm

added theorem CStarMatrix.normedSpaceCore:

deleted theorem CStarMatrix.normedSpaceCore

modified theorem CStarMatrix.toCLM_injective