Theorem AlgHom.norm_apply_le_self

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 View on Github →

2023-06-11 13:19

Mathlib/Analysis/NormedSpace/Spectrum.lean

feat: port Analysis.NormedSpace.Spectrum (#4946)

Added AlgHom.norm_apply_le_self View on Github →