Theorem NonUnitalStarAlgHom.norm_apply_le

Modification history

2024-08-08 16:24
Mathlib/Analysis/CStarAlgebra/Spectrum.lean
feat: star algebra homomorphisms between non-unital C⋆-algebras are contractive (#14544) …
Added NonUnitalStarAlgHom.norm_apply_leView on Github →