case mk
G : Type ?u.22201
H : Type ?u.22204
A : Type u_1
a a₁ a₂ b c : G
inst✝ : AddGroup A
s : Set A
h₁ : IsSubgroup s
h₂ : ∀ (n : Multiplicative A), n ∈ s → ∀ (g : Multiplicative A), g * n * g⁻¹ ∈ s
⊢ IsNormalAddSubgroup s
G : Type ?u.22201
H : Type ?u.22204
A : Type u_1
a a₁ a₂ b c : G
inst✝ : AddGroup A
s : Set A
⊢ IsNormalSubgroup s → IsNormalAddSubgroup s
rintro ⟨h₁, h₂⟩
no goals
case mk
G : Type ?u.22201
H : Type ?u.22204
A : Type u_1
a a₁ a₂ b c : G
inst✝ : AddGroup A
s : Set A
h₁ : IsSubgroup s
h₂ : ∀ (n : Multiplicative A), n ∈ s → ∀ (g : Multiplicative A), g * n * g⁻¹ ∈ s
⊢ IsNormalAddSubgroup s
exact @IsNormalAddSubgroup.mk A _ _ (Multiplicative.isSubgroup_iff.1 h₁) @h₂