Theorem: DividedPowerAlgebra.dp_mul (DividedPowers/DPAlgebra/Init.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ dp R n m * dp R p m = (n + p).choose n • dp R (n + p) m
Tactic:
simp only [dp_def, ← _root_.map_mul, ← map_nsmul]
State after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m) * X (p, m)) = (mkAlgHom R (Rel R M)) ((n + p).choose n • X (n + p, m))

State before:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n p : ℕ
m : M
⊢ (mkAlgHom R (Rel R M)) (X (n, m) * X (p, m)) = (mkAlgHom R (Rel R M)) ((n + p).choose n • X (n + p, m))
Tactic:
exact mkAlgHom_rel R Rel.mul
State after:
no goals