English
Let n be such that (n-1)! is a unit in A and I^n = 0. Then for all m,k with k ≠ 0, dpow I m (dpow I k x) equals uniformBell(m,k) times dpow I (m·k) x for x ∈ I.
Русский
Пусть n таково, что (n-1)! единично и I^n = 0. Тогда при любых m,k (k ≠ 0) dpow I m (dpow I k x) = uniformBell(m,k) · dpow I (m·k) x для x ∈ I.
LaTeX
$$$\text{IsUnit}((n-1)!:A) \to I^n = 0 \to \forall m,k, k \neq 0 \to x \in I, dpow\_I(m, dpow\_I(k, x)) = \mathrm{uniformBell}(m,k) \cdot dpow\_I(m k, x)$$$
Lean4
theorem dpow_comp {n : ℕ} (hn_fac : IsUnit ((n - 1).factorial : A)) (hnI : I ^ n = 0) {m k : ℕ} (hk : k ≠ 0) {x : A}
(hx : x ∈ I) : dpow I m (dpow I k x) = ↑(uniformBell m k) * dpow I (m * k) x :=
by
by_cases hmk : m * k < n
· exact dpow_comp_of_mul_lt hn_fac hk hmk hx
· have hxmk : x ^ (m * k) = 0 := Ideal.pow_eq_zero_of_mem hnI (not_lt.mp hmk) hx
rw [dpow_eq_of_mem (dpow_mem hk hx), dpow_eq_of_mem hx, dpow_eq_of_mem hx, mul_pow, ← pow_mul, ← mul_assoc,
mul_comm k, hxmk, mul_zero, mul_zero, mul_zero]
