Theorem: DividedPowerAlgebra.LinearMap.dp_add (DividedPowers/DPAlgebra/Init.lean)

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