English
Let n be a natural number such that (n−1)! is a unit in A. If m < n and x,y ∈ I, then dpow I m (x + y) equals the finite sum over the antidiagonal of m of dpow I k1 x times dpow I k2 y.
Русский
Пусть n натурально, и (n−1)! единичный элемент в A. Если m < n и x,y ∈ I, то dpow I m (x+y) равна сумме по антидиагонали m от dpow I k1 x умножить dpow I k2 y.
LaTeX
$$$\text{IsUnit}((n-1)!:A) \;\to\; (m < n) \to\; x,y \in I \Rightarrow dpow\_I(m, x+y) = \sum_{k \in \mathrm{antidiagonal}(m)} dpow\_I(k.1, x) \cdot dpow\_I(k.2, y)$$
Lean4
theorem dpow_add_of_lt {n : ℕ} (hn_fac : IsUnit ((n - 1)! : A)) {m : ℕ} (hmn : m < n) {x y : A} (hx : x ∈ I)
(hy : y ∈ I) : dpow I m (x + y) = (Finset.antidiagonal m).sum (fun k ↦ dpow I k.1 x * dpow I k.2 y) :=
by
rw [dpow_eq_of_mem (Ideal.add_mem I hx hy)]
simp only [dpow]
rw [inverse_mul_eq_iff_eq_mul _ _ _ (hn_fac.natCast_factorial_of_lt hmn), Finset.mul_sum,
Commute.add_pow' (Commute.all _ _)]
apply Finset.sum_congr rfl
intro k hk
rw [if_pos hx, if_pos hy]
ring_nf
simp only [mul_assoc]; congr; rw [← mul_assoc]
exact castChoose_eq (hn_fac.natCast_factorial_of_lt hmn) hk
