congr_symm — Mathlib

English

The inverse of congr G' H' e he is congr H' G' e^{-1} with the corresponding condition.

Русский

Обратное к congr G' H' e he — congr H' G' e^{-1} с соответствующим условием.

LaTeX

$$$(\\text{congr } G' H' e he)^{-1} = \\text{congr } H' G' e^{-1} ((\\text{Subgroup.map_symm_eq_iff_map_eq} _).mpr he)$$$

Lean4

@[simp]
theorem congr_symm (e : G ≃* H) (he : G'.map ↑e = H') :
    (congr G' H' e he).symm = congr H' G' e.symm ((Subgroup.map_symm_eq_iff_map_eq _).mpr he) :=
  rfl

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