Theorem NonUnitalStarAlgHom.nnnorm_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.nnnorm_apply_leView on Github →