ofMul_image_zpowers_eq_zmultiples_ofMul

English

The image of zpowers x under the additive functor of multiplication equals the subgroup of multiples of Additive.ofMul x: Additive.ofMul '' (Subgroup.zpowers x) = AddSubgroup.zmultiples (Additive.ofMul x).

Русский

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

LaTeX

$$$\operatorname{Additive.ofMul} '' (\operatorname{zpowers}(x)) = \operatorname{AddSubgroup.zmultiples}(\operatorname{Additive.ofMul}(x))$$$

Lean4

theorem ofMul_image_zpowers_eq_zmultiples_ofMul {x : G} :
    Additive.ofMul '' (Subgroup.zpowers x : Set G) = AddSubgroup.zmultiples (Additive.ofMul x) :=
  by
  ext
  exact Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

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