Theorem: DividedPowers.OfInvertibleFactorial.dpow_smul (DividedPowers/RatAlgebra.lean)

State before:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m : ℕ
a x : A
hx : x ∈ I
⊢ dpow I m (a * x) = a ^ m * dpow I m x
Tactic:
rw [dpow_eq_of_mem m (Ideal.mul_mem_left I _ hx), dpow_eq_of_mem m hx,
  mul_pow, ← mul_assoc, mul_comm _ (a ^ m), mul_assoc]
State after:
no goals