English
If n is such that (n-1)! is a unit in A, k ≠ 0, and m·k < n, then dpow I m (dpow I k x) = uniformBell(m,k) · dpow I (m·k) x for x ∈ I.
Русский
Пусть n таково, что (n-1)! единично, k ≠ 0 и m·k < n; тогда dpow I m (dpow I k x) = uniformBell(m,k) · dpow I (m·k) x при x ∈ I.
LaTeX
$$$\text{IsUnit}((n-1)!:A) \to k \neq 0 \to m k < n \to x \in I \Rightarrow dpow\_I(m, dpow\_I(k, x)) = \uparrow(\mathrm{uniformBell}(m,k)) dpow\_I(m k, x)$$$
Lean4
theorem dpow_comp_of_mul_lt {n : ℕ} (hn_fac : IsUnit ((n - 1)! : A)) {m k : ℕ} (hk : k ≠ 0) (hkm : m * k < n) {x : A}
(hx : x ∈ I) : dpow I m (dpow I k x) = ↑(uniformBell m k) * dpow I (m * k) x :=
by
have hmn : m < n := lt_of_le_of_lt (Nat.le_mul_of_pos_right _ (Nat.pos_of_ne_zero hk)) hkm
rw [dpow_eq_of_mem (m := m * k) hx, dpow_eq_of_mem (dpow_mem hk hx)]
by_cases hm0 : m = 0
· simp only [hm0, zero_mul, _root_.pow_zero, mul_one, uniformBell_zero_left, cast_one, one_mul]
· have hkn : k < n := lt_of_le_of_lt (Nat.le_mul_of_pos_left _ (Nat.pos_of_ne_zero hm0)) hkm
rw [dpow_eq_of_mem hx, mul_pow, ← pow_mul, mul_comm k, ← mul_assoc, ← mul_assoc]
apply congr_arg₂ _ _ rfl
rw [eq_mul_inverse_iff_mul_eq _ _ _ (hn_fac.natCast_factorial_of_lt hkm), mul_assoc,
inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hmn),
inverse_pow_mul_eq_iff_eq_mul _ _ (hn_fac.natCast_factorial_of_lt hkn), ← uniformBell_mul_eq _ hk]
simp only [Nat.cast_mul, Nat.cast_pow]
ring_nf
