feat(normed_space/normed_group_hom): add lemmas (#7468)

From LTE.

Written by @PatrickMassot 



Co-authored-by: Patrick Massot <patrickmassot@free.fr>

src/analysis/normed_space/normed_group_hom.lean

@@ -434,6 +434,16 @@ by { erw f.to_add_monoid_hom.mem_ker, refl }
   (incl g.ker).comp (ker.lift f g h) = f :=
 by { ext, refl }
 
+@[simp]
+lemma ker_zero : (0 : normed_group_hom V₁ V₂).ker = ⊤ :=
+by { ext, simp [mem_ker] }
+
+lemma coe_ker : (f.ker : set V₁) = (f : V₁ → V₂) ⁻¹' {0} := rfl
+
+lemma is_closed_ker {V₂ : Type*} [normed_group V₂] (f : normed_group_hom V₁ V₂) :
+  is_closed (f.ker : set V₁) :=
+f.coe_ker ▸ is_closed.preimage f.continuous (t1_space.t1 0)
+
 end kernels
 
 /-! ### Range -/

src/group_theory/subgroup.lean

@@ -1255,6 +1255,9 @@ def ker (f : G →* N) := (⊥ : subgroup N).comap f
 @[to_additive]
 lemma mem_ker (f : G →* N) {x : G} : x ∈ f.ker ↔ f x = 1 := iff.rfl
 
+@[to_additive]
+lemma coe_ker (f : G →* N) : (f.ker : set G) = (f : G → N) ⁻¹' {1} := rfl
+
 @[to_additive]
 instance decidable_mem_ker [decidable_eq N] (f : G →* N) :
   decidable_pred (∈ f.ker) :=
@@ -1270,6 +1273,10 @@ begin
   simp only [],
 end
 
+@[simp, to_additive]
+lemma ker_one : (1 : G →* N).ker = ⊤ :=
+by { ext, simp [mem_ker] }
+
 @[to_additive] lemma ker_eq_bot_iff (f : G →* N) : f.ker = ⊥ ↔ function.injective f :=
 begin
   split,