coe_subgroupMap_apply — Mathlib

English

The action of subgroupMap on an element g ∈ H maps to the image under e, exactly e(g).

Русский

Действие subgroupMap на элемент g ∈ H даёт образ этого элемента через e: равняется e(g).

LaTeX

$$$((\\operatorname{subgroupMap}(e)\\, H\\, g) : H.map (e)) = e(g)$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_subgroupMap_apply (e : G ≃* G') (H : Subgroup G) (g : H) :
    ((subgroupMap e H g : H.map (e : G →* G')) : G') = e g :=
  rfl

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