Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-15 13:15 0597b1dd

View on Github →

feat(analysis/normed_space/normed_group_hom): add equalizer (#8228) From LTE. We add equalizer of normed_group_homs.

Estimated changes

Modified src/analysis/normed_space/normed_group_hom.lean

added theorem normed_group_hom.equalizer.comm_sq₂

added theorem normed_group_hom.equalizer.comp_ι_eq

added def normed_group_hom.equalizer.lift

added def normed_group_hom.equalizer.lift_equiv

added theorem normed_group_hom.equalizer.lift_norm_noninc

added def normed_group_hom.equalizer.map

added theorem normed_group_hom.equalizer.map_comp_map

added theorem normed_group_hom.equalizer.map_id

added theorem normed_group_hom.equalizer.map_norm_noninc

added theorem normed_group_hom.equalizer.norm_lift_le

added theorem normed_group_hom.equalizer.norm_map_le

added def normed_group_hom.equalizer.ι

added theorem normed_group_hom.equalizer.ι_comp_lift

added theorem normed_group_hom.equalizer.ι_comp_map

added theorem normed_group_hom.equalizer.ι_norm_noninc

added def normed_group_hom.equalizer