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

State before:
R : Type u_4
M : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
S : Type u_1
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
inst✝¹ : Algebra R (DividedPowerAlgebra S N)
inst✝ : IsScalarTower R S (DividedPowerAlgebra S N)
f : M →ₗ[R] N
n : ℕ
a b : M
⊢ dp S n (f (a + b)) = ∑ k ∈ range (n + 1), dp S k (f a) * dp S (n - k) (f b)
Tactic:
rw [map_add, DividedPowerAlgebra.dp_add]
State after:
no goals