ofAdd_image_multiples_eq_powers_ofAdd

English

The image of AddSubmonoid multiples under the ofAdd equivalence equals the powers in AddSubmonoid.

Русский

Образ множителей AddSubmonoid multiples через эквивалентность ofAdd совпадает со степенями в AddSubmonoid.

LaTeX

$$$ (\\text{image of Additive.ofAdd}) (AddSubmonoid.multiples x) = \\operatorname{powers}(\\text{Additive.ofAdd } x) $$$

Lean4

theorem ofAdd_image_multiples_eq_powers_ofAdd [AddMonoid A] {x : A} :
    Multiplicative.ofAdd '' (AddSubmonoid.multiples x : Set A) = Submonoid.powers (Multiplicative.ofAdd x) :=
  by
  symm
  rw [Equiv.eq_image_iff_symm_image_eq]
  exact ofMul_image_powers_eq_multiples_ofMul

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