Theorem IsGreatest.pi_norm'

Modification history

2026-06-24 17:51
Mathlib/Analysis/Normed/Group/Constructions.lean
feat(CStarAlgebra): `IsometricCFC` instance for square `RCLike` matrices (#40272) …
Added IsGreatest.pi_norm'View on Github →