Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-07 04:59 9acbe588

View on Github →

feat(normed_space/normed_group_hom): add lemmas (#7468) From LTE. Written by @PatrickMassot

Estimated changes

Modified src/analysis/normed_space/normed_group_hom.lean

added theorem normed_group_hom.coe_ker

added theorem normed_group_hom.is_closed_ker

added theorem normed_group_hom.ker_zero

Modified src/group_theory/subgroup.lean

added theorem monoid_hom.coe_ker

added theorem monoid_hom.ker_one