G : Type u_1
G' : Type ?u.352996
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.353005
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.352996
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.353005
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.352996
inst✝² : Group G
inst✝¹ : Group G'
A : Type ?u.353005
inst✝ : AddGroup A
H K : Subgroup G
⊢ Characteristic H ↔ ∀ (ϕ : G ≃* G), comap (MulEquiv.toMonoidHom (MulEquiv.symm ϕ)) H ≤ H
exact characteristic_iff_comap_le.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩