equivMapOfInjective_coe_mulEquiv — Mathlib

English

The explicit description of an equivalence between H and its image, arising from an injective map f, agrees with the MulEquiv-based subgroup equivalence after identifying the ambient types.

Русский

Ясное описание эквивалентности между H и её изображением, полученной из инъективного отображения f, согласуется с эквив подгрупп MulEquiv после идентификации окружающих типов.

LaTeX

$$$H\\\\equivMapOfInjective f hf = e.subgroupMap H$$$

Lean4

@[to_additive (attr := simp)]
theorem equivMapOfInjective_coe_mulEquiv (H : Subgroup G) (e : G ≃* G') :
    H.equivMapOfInjective (e : G →* G') (EquivLike.injective e) = e.subgroupMap H :=
  by
  ext
  rfl

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