G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutatorSet G ⊆ ↑(MonoidHom.ker f)
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutator G ≤ MonoidHom.ker f
rw [commutator_eq_closure, Subgroup.closure_le]
case intro.intro
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
p q : G
⊢ ⁅p, q⁆ ∈ ↑(MonoidHom.ker f)
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutatorSet G ⊆ ↑(MonoidHom.ker f)
rintro x ⟨p, q, rfl⟩
no goals
case intro.intro
G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
p q : G
⊢ ⁅p, q⁆ ∈ ↑(MonoidHom.ker f)
simp [MonoidHom.mem_ker, mul_right_comm (f p) (f q), commutatorElement_def]