Theorem: DividedPowers.dpow_smul' (DividedPowers/Basic.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
n : ℕ
a x : A
hx : x ∈ I
⊢ hI.dpow n (a • x) = a ^ n • hI.dpow n x
Tactic:
simp only [smul_eq_mul, hI.dpow_smul, hx]
State after:
no goals