M : Type ?u.302290
A : Type u_1
B : Type ?u.302296
inst✝ : AddMonoid A
x : A
⊢ ↑(Submonoid.powers (↑Multiplicative.ofAdd x)) = ↑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x)
M : Type ?u.302290
A : Type u_1
B : Type ?u.302296
inst✝ : AddMonoid A
x : A
⊢ ↑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x) = ↑(Submonoid.powers (↑Multiplicative.ofAdd x))
symm
M : Type ?u.302290
A : Type u_1
B : Type ?u.302296
inst✝ : AddMonoid A
x : A
⊢ ↑Multiplicative.ofAdd.symm '' ↑(Submonoid.powers (↑Multiplicative.ofAdd x)) = ↑(AddSubmonoid.multiples x)
M : Type ?u.302290
A : Type u_1
B : Type ?u.302296
inst✝ : AddMonoid A
x : A
⊢ ↑(Submonoid.powers (↑Multiplicative.ofAdd x)) = ↑Multiplicative.ofAdd '' ↑(AddSubmonoid.multiples x)
rw [Equiv.eq_image_iff_symm_image_eq]
no goals
M : Type ?u.302290
A : Type u_1
B : Type ?u.302296
inst✝ : AddMonoid A
x : A
⊢ ↑Multiplicative.ofAdd.symm '' ↑(Submonoid.powers (↑Multiplicative.ofAdd x)) = ↑(AddSubmonoid.multiples x)
exact ofMul_image_powers_eq_multiples_ofMul