∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {n : ℕ},
  IsUnit ↑(n - 1).factorial →
    I ^ n = 0 →
      ∀ {m : ℕ} {x : A},
        x ∈ I →
          ∀ {y : A},
            y ∈ I →
              DividedPowers.OfInvertibleFactorial.dpow I m (x + y) =
                ∑ k ∈ Finset.antidiagonal m,
                  DividedPowers.OfInvertibleFactorial.dpow I k.1 x * DividedPowers.OfInvertibleFactorial.dpow I k.2 y