subgroupMap_symm_apply — Mathlib

English

The inverse of subgroupMap is the corresponding inverse map applied to an element of the image.

Русский

Обратное отображение subgroupMap применяется к элементу образа через соответствующую инверсию.

LaTeX

$$$(\\operatorname{subgroupMap}(e)).\\mathrm{symm}(g) = \\langle e^{-1}(g), \\text{ evidence} \\rangle$$$

Lean4

@[to_additive (attr := simp)]
theorem subgroupMap_symm_apply (e : G ≃* G') (H : Subgroup G) (g : H.map (e : G →* G')) :
    (e.subgroupMap H).symm g = ⟨e.symm g, SetLike.mem_coe.1 <| Set.mem_image_equiv.1 g.2⟩ :=
  rfl

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