English
For commuting x, y in a ring and m ≤ n, the product (sum over i in Ico m n of x^i y^{n-1-i}) times (x − y) equals x^n − y^{n−m} x^m.
Русский
Пусть x и y коммутируют в кольце и m ≤ n. Тогда произведение суммы по i в Ico m n от x^i y^{n-1-i} на (x − y) равно x^n − y^{n-m} x^m.
LaTeX
$$$\\displaystyle (\\sum_{i \\in \\mathrm{Ico}(m,n)} x^i y^{n-1-i})(x - y) = x^n - y^{n-m} x^m$$$
Lean4
protected theorem mul_geom_sum₂_Ico (h : Commute x y) {m n : ℕ} (hmn : m ≤ n) :
((x - y) * ∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) = x ^ n - x ^ m * y ^ (n - m) :=
by
rw [sum_Ico_eq_sub _ hmn]
have : ∑ k ∈ range m, x ^ k * y ^ (n - 1 - k) = ∑ k ∈ range m, x ^ k * (y ^ (n - m) * y ^ (m - 1 - k)) :=
by
refine sum_congr rfl fun j j_in => ?_
rw [← pow_add]
congr
rw [mem_range] at j_in
omega
rw [this]
simp_rw [pow_mul_comm y (n - m) _]
simp_rw [← mul_assoc]
rw [← sum_mul, mul_sub, h.mul_geom_sum₂, ← mul_assoc, h.mul_geom_sum₂, sub_mul, ← pow_add, add_tsub_cancel_of_le hmn,
sub_sub_sub_cancel_right (x ^ n) (x ^ m * y ^ (n - m)) (y ^ n)]
