Lemmas about pointwise operations in the presence of Multiplicative and Additive.

@[simp]

theorem Multiplicative.ofAdd_image_setAdd {M : Type u_1} [AddMonoid M] (s t : Set M) : ⇑ofAdd '' (s + t) = ⇑ofAdd '' s * ⇑ofAdd '' t

@[simp]

theorem Multiplicative.ofAdd_image_nsmul {M : Type u_1} [AddMonoid M] (n : ℕ) (s : Set M) : ⇑ofAdd '' (n • s) = (⇑ofAdd '' s) ^ n

@[simp]

theorem Multiplicative.toAdd_image_setMul {M : Type u_1} [AddMonoid M] (s t : Set (Multiplicative M)) : ⇑toAdd '' (s * t) = ⇑toAdd '' s + ⇑toAdd '' t

@[simp]

theorem Multiplicative.toAdd_image_nsmul {M : Type u_1} [AddMonoid M] (n : ℕ) (s : Set (Multiplicative M)) : ⇑toAdd '' s ^ n = n • ⇑toAdd '' s