feat(group_theory/subgroup/basic): Kernel of subtype and inclusion (

#9763)

`subtype` and `inculusion` are injective, so they have trivial kernel.

src/group_theory/subgroup/basic.lean

@@ -1532,6 +1532,13 @@ begin
   { exact λ h, le_bot_iff.mp (λ x hx, h (hx.trans f.map_one.symm)) },
 end
 
+@[simp, to_additive] lemma _root_.subgroup.ker_subtype (H : subgroup G) : H.subtype.ker = ⊥ :=
+H.subtype.ker_eq_bot_iff.mpr subtype.coe_injective
+
+@[simp, to_additive] lemma _root_.subgroup.ker_inclusion {H K : subgroup G} (h : H ≤ K) :
+  (inclusion h).ker = ⊥ :=
+(inclusion h).ker_eq_bot_iff.mpr (set.inclusion_injective h)
+
 @[to_additive]
 lemma prod_map_comap_prod {G' : Type*} {N' : Type*} [group G'] [group N']
   (f : G →* N) (g : G' →* N') (S : subgroup N) (S' : subgroup N') :