Theorem Function.Surjective.pi_norm_comp'

Modification history

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