Lemmas about ℤᵐ⁰.

@[deprecated WithZero.exp_zsmul (since := "2025-05-17")]

theorem WithZero.ofAdd_zpow (a : ℤ) : ↑(Multiplicative.ofAdd a) = ↑(Multiplicative.ofAdd 1) ^ a

@[deprecated WithZero.exp_neg (since := "2025-05-17")]

theorem WithZero.ofAdd_neg_one_pow_comm (a : ℤ) (n : ℕ) : (↑(Multiplicative.ofAdd (-1)) ^ (-a)) ^ n = ↑(Multiplicative.ofAdd ↑n) ^ a