Theorem AlgHom.norm_apply_le_self_mul_norm_one

Modification history

2024-02-05 18:00
Mathlib/Analysis/NormedSpace/Spectrum.lean
refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …
Modified AlgHom.norm_apply_le_self_mul_norm_oneView on Github →
2023-06-11 13:19
Mathlib/Analysis/NormedSpace/Spectrum.lean
feat: port Analysis.NormedSpace.Spectrum (#4946)
Added AlgHom.norm_apply_le_self_mul_norm_oneView on Github →