English
In a divided powers construction, the m-th divided power of x+y equals the sum over antidiagonal terms of x and y powers, provided a factorial condition holds.
Русский
В конструкции делённых степеней m-я делённая степень x+y равна сумме по антидиагонали произведений степеней x и y, при условии факториала.
LaTeX
$$$\text{dpow } I m (x+y) = (\text{antidiagonal}(m)) \sum_{k} dpow I k.1 x \cdot dpow I k.2 y$$$
Lean4
theorem dpow_add {n : ℕ} (hn_fac : IsUnit ((n - 1)! : A)) (hnI : I ^ n = 0) {m : ℕ} {x : A} (hx : x ∈ I) {y : A}
(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
by_cases hmn : m < n
· exact dpow_add_of_lt hn_fac hmn hx hy
· have h_sub : I ^ m ≤ I ^ n := Ideal.pow_le_pow_right (not_lt.mp hmn)
rw [dpow_eq_of_mem (Ideal.add_mem I hx hy)]
simp only [dpow]
have hxy : (x + y) ^ m = 0 := by
rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
exact Set.mem_of_subset_of_mem h_sub (Ideal.pow_mem_pow (Ideal.add_mem I hx hy) m)
rw [hxy, mul_zero, eq_comm]
apply Finset.sum_eq_zero
intro k hk
rw [if_pos hx, if_pos hy, mul_assoc, mul_comm (x ^ k.1), mul_assoc, ← mul_assoc]
apply mul_eq_zero_of_right
rw [← Ideal.mem_bot, ← Ideal.zero_eq_bot, ← hnI]
apply Set.mem_of_subset_of_mem h_sub
rw [← Finset.mem_antidiagonal.mp hk, add_comm, pow_add]
exact Ideal.mul_mem_mul (Ideal.pow_mem_pow hy _) (Ideal.pow_mem_pow hx _)
