G : Type u_1
G' : Type ?u.351493
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.351502
inst✝ : AddGroup A
H K : Subgroup G
⊢ Characteristic H ↔ ∀ (ϕ : G ≃* G), comap (MulEquiv.toMonoidHom (MulEquiv.symm ϕ)) H = H
G : Type u_1
G' : Type ?u.351493
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.351502
inst✝ : AddGroup A
H K : Subgroup G
⊢ Characteristic H ↔ ∀ (ϕ : G ≃* G), map (MulEquiv.toMonoidHom ϕ) H = H
simp_rw [map_equiv_eq_comap_symm]
no goals
G : Type u_1
G' : Type ?u.351493
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.351502
inst✝ : AddGroup A
H K : Subgroup G
⊢ Characteristic H ↔ ∀ (ϕ : G ≃* G), comap (MulEquiv.toMonoidHom (MulEquiv.symm ϕ)) H = H
exact characteristic_iff_comap_eq.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩