mathlib3
0597b1dd - feat(analysis/normed_space/normed_group_hom): add equalizer (#8228)

Commit
4 years ago
feat(analysis/normed_space/normed_group_hom): add equalizer (#8228) From LTE. We add equalizer of `normed_group_homs`.
Parents
Loading