coe_mapSubgroup — Mathlib

English

The forward-subgroup map defined by an isomorphism e coincides with Subgroup.map on the underlying monoid hom, i.e., mapSubgroup e = Subgroup.map e.toMonoidHom.

Русский

Прямое отображение подгрупп, заданное изоморфизмом e, совпадает с отображением Subgroup.map через соответствующий моноид-гомоморфизм: mapSubgroup e = Subgroup.map e.toMonoidHom.

LaTeX

$$$\\operatorname{mapSubgroup}(e) = \\operatorname{Subgroup.map}(e^{\\mathrm{toMonoidHom}})$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_mapSubgroup (e : G ≃* H) : mapSubgroup e = Subgroup.map e.toMonoidHom :=
  rfl

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