∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (dpow : ℕ → A → A)
  (dpow_null : ∀ {n : ℕ} {x : A}, x ∉ I → dpow n x = 0) (dpow_zero : ∀ {x : A}, x ∈ I → dpow 0 x = 1)
  (dpow_one : ∀ {x : A}, x ∈ I → dpow 1 x = x) (dpow_mem : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow n x ∈ I)
  (dpow_add :
    ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → dpow n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow k.1 x * dpow k.2 y)
  (dpow_mul : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow n (a * x) = a ^ n * dpow n x)
  (mul_dpow : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow m x * dpow n x = ↑((m + n).choose m) * dpow (m + n) x)
  (dpow_comp : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow m (dpow n x) = ↑(m.uniformBell n) * dpow (m * n) x)
  (dpow_1 : ℕ → A → A) (dpow_null_1 : ∀ {n : ℕ} {x : A}, x ∉ I → dpow_1 n x = 0)
  (dpow_zero_1 : ∀ {x : A}, x ∈ I → dpow_1 0 x = 1) (dpow_one_1 : ∀ {x : A}, x ∈ I → dpow_1 1 x = x)
  (dpow_mem_1 : ∀ {n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow_1 n x ∈ I)
  (dpow_add_1 :
    ∀ {n : ℕ} {x y : A}, x ∈ I → y ∈ I → dpow_1 n (x + y) = ∑ k ∈ Finset.antidiagonal n, dpow_1 k.1 x * dpow_1 k.2 y)
  (dpow_mul_1 : ∀ {n : ℕ} {a x : A}, x ∈ I → dpow_1 n (a * x) = a ^ n * dpow_1 n x)
  (mul_dpow_1 : ∀ {m n : ℕ} {x : A}, x ∈ I → dpow_1 m x * dpow_1 n x = ↑((m + n).choose m) * dpow_1 (m + n) x)
  (dpow_comp_1 : ∀ {m n : ℕ} {x : A}, n ≠ 0 → x ∈ I → dpow_1 m (dpow_1 n x) = ↑(m.uniformBell n) * dpow_1 (m * n) x),
  ({ dpow := dpow, dpow_null := dpow_null, dpow_zero := dpow_zero, dpow_one := dpow_one, dpow_mem := dpow_mem,
        dpow_add := dpow_add, dpow_mul := dpow_mul, mul_dpow := mul_dpow, dpow_comp := dpow_comp } =
      { dpow := dpow_1, dpow_null := dpow_null_1, dpow_zero := dpow_zero_1, dpow_one := dpow_one_1,
        dpow_mem := dpow_mem_1, dpow_add := dpow_add_1, dpow_mul := dpow_mul_1, mul_dpow := mul_dpow_1,
        dpow_comp := dpow_comp_1 }) =
    (dpow = dpow_1)