Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-21 08:39 abdc3164

View on Github →

feat(analysis/normed_space/normed_group_hom): add lemmas (#7875) From LTE.

Estimated changes

Modified src/analysis/normed_space/SemiNormedGroup.lean

Modified src/analysis/normed_space/normed_group_hom.lean

added theorem normed_group_hom.coe_comp

added theorem normed_group_hom.coe_id

added theorem normed_group_hom.comp_assoc

modified theorem normed_group_hom.isometry_id

added theorem normed_group_hom.norm_comp_le_of_le'

added theorem normed_group_hom.norm_comp_le_of_le

modified theorem normed_group_hom.norm_id

modified theorem normed_group_hom.norm_id_le

modified theorem normed_group_hom.norm_noninc.id