Theorem: DividedPowers.dpow_smul_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 [smul_eq_mul, hI.dpow_mul_right n ha, smul_eq_mul]
State after:
no goals