toSubgroup_comap — Mathlib

English

The additive-to-subgroup correspondence preserves comap along a monoid homomorphism.

Русский

Соответствие аддитивного к подгруппе сохраняет comap вдоль моноид-гомоморфизма.

LaTeX

$$$ (s : AddSubgroup A_2) .toSubgroup.comap (AddMonoidHom.toMultiplicative f) = AddSubgroup.toSubgroup (s.comap f) $$$

Lean4

@[simp]
theorem _root_.AddSubgroup.toSubgroup_comap {A A₂ : Type*} [AddGroup A] [AddGroup A₂] (f : A →+ A₂)
    (s : AddSubgroup A₂) : s.toSubgroup.comap (AddMonoidHom.toMultiplicative f) = AddSubgroup.toSubgroup (s.comap f) :=
  rfl

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