toAddSubgroup_comap — Mathlib

English

The correspondence between additive and multiplicative preimages respects the comap operation.

Русский

Соответствие между предобразами в аддитивной и мультипликативной точках зрения сохраняет операцию comap.

LaTeX

$$$ \\text{toAddSubgroup_comap: additive-to-multiplicative correspondence commutes with comap.} $$$

Lean4

@[simp]
theorem toAddSubgroup_comap {G₂ : Type*} [Group G₂] (f : G →* G₂) (s : Subgroup G₂) :
    s.toAddSubgroup.comap (MonoidHom.toAdditive f) = Subgroup.toAddSubgroup (s.comap f) :=
  rfl

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