G : Type u_1
H : Type u_2
A : Type ?u.115479
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
⊢ (∀ (x : G), x ∈ ker f ↔ x ∈ IsSubgroup.trivial G) ↔ ∀ (x : G), f x = 1 → x = 1
G : Type u_1
H : Type u_2
A : Type ?u.115479
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
⊢ ker f = IsSubgroup.trivial G ↔ ∀ (x : G), f x = 1 → x = 1
rw [Set.ext_iff]
G : Type u_1
H : Type u_2
A : Type ?u.115479
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
⊢ (∀ (x : G), f x = 1 ↔ x = 1) ↔ ∀ (x : G), f x = 1 → x = 1
G : Type u_1
H : Type u_2
A : Type ?u.115479
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
⊢ (∀ (x : G), x ∈ ker f ↔ x ∈ IsSubgroup.trivial G) ↔ ∀ (x : G), f x = 1 → x = 1
simp [ker]
no goals
G : Type u_1
H : Type u_2
A : Type ?u.115479
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
⊢ (∀ (x : G), f x = 1 ↔ x = 1) ↔ ∀ (x : G), f x = 1 → x = 1
exact ⟨fun h x hx => (h x).1 hx, fun h x => ⟨h x, fun hx => by rw [hx, hf.map_one]⟩⟩
no goals
G : Type u_1
H : Type u_2
A : Type ?u.115479
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : ∀ (x : G), f x = 1 → x = 1
x : G
hx : x = 1
⊢ f x = 1
rw [hx, hf.map_one]