Lemmas about Multiplicative ℤ.

theorem Int.toAdd_pow (a : Multiplicative ℤ) (b : ℕ) : Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * ↑b

theorem Int.toAdd_zpow (a : Multiplicative ℤ) (b : ℤ) : Multiplicative.toAdd (a ^ b) = Multiplicative.toAdd a * b

@[simp]

theorem Int.ofAdd_mul (a b : ℤ) : Multiplicative.ofAdd (a * b) = Multiplicative.ofAdd a ^ b