Theorem: DividedPowerAlgebra.dp_add (unused_files/Init_copy.lean)

State before:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ dp R n (x + y) = ∑ k ∈ range (n + 1), dp R k x * dp R (n - k) y
Tactic:
simp only [dp_def]
State after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x y : M
⊢ (mkAlgHom R (Rel R M)) (X (n, x + y)) =
    ∑ x_1 ∈ range (n + 1), (mkAlgHom R (Rel R M)) (X (x_1, x)) * (mkAlgHom R (Rel R M)) (X (n - x_1, y))