subgroupMap_surjective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem subgroupMap_surjective (f : G →* G') (H : Subgroup G) : Function.Surjective (f.subgroupMap H) :=
  f.submonoidMap_surjective H.toSubmonoid

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