ofMul_image_powers_eq_multiples_ofMul

English

The image of powers under the Additive ofMul correspondence equals the set of multiples of the additive base.

Русский

Образ степеней через соответствие ofMul равен множеству кратных базовому элементу.

LaTeX

$$$ Additive.ofMul '' (\\operatorname{powers} x) = AddSubmonoid.multiples (Additive.ofMul x) $$$

Lean4

theorem ofMul_image_powers_eq_multiples_ofMul [Monoid M] {x : M} :
    Additive.ofMul '' (Submonoid.powers x : Set M) = AddSubmonoid.multiples (Additive.ofMul x) :=
  by
  ext
  exact Set.mem_image_iff_of_inverse (congrFun rfl) (congrFun rfl)

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