Theorem ContinuousMap.norm_eq_norm_coeFn

Modification history

2026-06-24 17:51
Mathlib/Topology/ContinuousMap/Compact.lean
feat(CStarAlgebra): `IsometricCFC` instance for square `RCLike` matrices (#40272) …
Added ContinuousMap.norm_eq_norm_coeFnView on Github →