map_symm_eq_iff_map_eq — Mathlib

English

Let f be a MulEquiv G N. Then K.map (f) = K.comap (f.symm).

Русский

Пусть f — MulEquiv G N. Тогда K.map f = K.comap f.symm.

LaTeX

$$map_equiv_eq_comap_symm (f) (K) =$$

Lean4

@[to_additive]
theorem map_symm_eq_iff_map_eq {H : Subgroup N} {e : G ≃* N} : H.map ↑e.symm = K ↔ K.map ↑e = H :=
  by
  constructor <;> rintro rfl
  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.symm_trans_self, MulEquiv.coe_monoidHom_refl, map_id]
  · rw [map_map, ← MulEquiv.coe_monoidHom_trans, MulEquiv.self_trans_symm, MulEquiv.coe_monoidHom_refl, map_id]

Похожие утверждения