{A : Type u_1} →
  [inst : CommSemiring A] →
    {I : Ideal A} →
      (dpow : ℕ → A → A) →
        (∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) →
          (∀ {x : A}, x ∈ I → dpow 0 x = 1) →
            (∀ {x : A}, x ∈ I → dpow 1 x = x) →
              (∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I) →
                (∀ {n : ℕ} {x y : A},
                    x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow k.1 x * dpow k.2 y) →
                  (∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x) →
                    (∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x) →
                      (∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x) →
                        DividedPowers I