Theorem: DividedPowers.dpow_mul_right (DividedPowers/Basic.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
a : A
ha : a ∈ I
x : A
⊢ hI.dpow n (a * x) = hI.dpow n a * x ^ n
Tactic:
rw [mul_comm, hI.dpow_smul n ha, mul_comm]
State after:
no goals