Theorem: DividedPowerAlgebra.dp_comp (DividedPowers/DPAlgebra/Dpow.lean)

State before:
A : Type u
inst✝³ : CommRing A
inst✝² : DecidableEq A
M : Type u
inst✝¹ : AddCommGroup M
inst✝ : Module A M
x : M
n m : ℕ
hn : n ≠ 0
⊢ (dividedPowers' A M).dpow m (dp A n x) = ↑(mchoose m n) * dp A (m * n) x
Tactic:
erw [← (roby_D A M).choose_spec, dpow_comp _ m hn (ι_mem_augIdeal A M x), dpow_ι]
State after:
no goals