Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-26 20:25 5ef64261

View on Github →

feat(analysis/normed_space/star/spectrum): star algebra morphisms over ℂ are norm contractive (#16219)

depends on: #16177
depends on: #16212

Estimated changes

Modified src/analysis/normed_space/star/spectrum.lean

added theorem star_alg_hom.nnnorm_apply_le

added theorem star_alg_hom.norm_apply_le