Theorem pi_norm_comp_le'

Modification history

2026-10-02 14:34
Mathlib/Analysis/Normed/Group/Constructions.lean
feat(Analysis/Normed): sup norm of Function.extend by one (#44378)
Modified pi_norm_comp_le'View on Github →
2026-06-24 17:51
Mathlib/Analysis/Normed/Group/Constructions.lean
feat(CStarAlgebra): `IsometricCFC` instance for square `RCLike` matrices (#40272) …
Added pi_norm_comp_le'View on Github →