symm_mapSubgroup — Mathlib

English

The inverse of the forward subgroup map equals the forward subgroup map of the inverse isomorphism: (mapSubgroup e).symm = mapSubgroup e.symm.

Русский

Обратное к отображению подгрупп по факту — равно отображению подгрупп по обратному изоморфизму: (mapSubgroup e).symm = mapSubgroup e.symm.

LaTeX

$$$(\\operatorname{mapSubgroup}(e)).\\mathrm{symm} = \\operatorname{mapSubgroup}(e^{-1})$$$

Lean4

@[to_additive (attr := simp)]
theorem symm_mapSubgroup (e : G ≃* H) : (mapSubgroup e).symm = mapSubgroup e.symm :=
  rfl

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