∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (self : DividedPowers I) {n : ℕ} {x y : A},
  x ∈ I → y ∈ I → self.dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, self.dpow k.1 x * self.dpow k.2 y