ofAdd_image_zmultiples_eq_zpowers_ofAdd

English

The image of zmultiples x under Multiplicative.ofAdd equals zpowers (Multiplicative.ofAdd x): Multiplicative.ofAdd '' (AddSubgroup.zmultiples x) = Subgroup.zpowers (Multiplicative.ofAdd x).

Русский

Образ zmultiples(x) под отображением Multiplicative.ofAdd равен zpowers(Multiplicative.ofAdd x).

LaTeX

$$$\operatorname{Multiplicative.ofAdd} '' (\operatorname{AddSubgroup.zmultiples} x) = \operatorname{Subgroup.zpowers}(\operatorname{Multiplicative.ofAdd} x)$$$

Lean4

theorem ofAdd_image_zmultiples_eq_zpowers_ofAdd {x : A} :
    Multiplicative.ofAdd '' (AddSubgroup.zmultiples x : Set A) = Subgroup.zpowers (Multiplicative.ofAdd x) :=
  by
  symm
  rw [Equiv.eq_image_iff_symm_image_eq]
  exact ofMul_image_zpowers_eq_zmultiples_ofMul

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