English
For commuting x, y and m ≤ n, the Ico-based sum times (x − y) equals x^n − y^{n-m} x^m.
Русский
Для коммутируемых x, y и m ≤ n сумма по Ico умноженная на (x − y) даёт x^n − y^{n-m} x^m.
LaTeX
$$$\\displaystyle \\left(\\sum_{i \\in \\mathrm{Ico}(m,n)} x^i y^{n-1-i}\\right) (x - y) = x^n - y^{n-m} x^m$$$
Lean4
protected theorem geom_sum₂_Ico_mul (h : Commute x y) {m n : ℕ} (hmn : m ≤ n) :
(∑ i ∈ Finset.Ico m n, x ^ i * y ^ (n - 1 - i)) * (x - y) = x ^ n - y ^ (n - m) * x ^ m :=
by
apply op_injective
simp only [op_sub, op_mul, op_pow, op_sum]
have :
(∑ k ∈ Ico m n, MulOpposite.op y ^ (n - 1 - k) * MulOpposite.op x ^ k) =
∑ k ∈ Ico m n, MulOpposite.op x ^ k * MulOpposite.op y ^ (n - 1 - k) :=
by
refine sum_congr rfl fun k _ => ?_
have hp := Commute.pow_pow (Commute.op h.symm) (n - 1 - k) k
simpa [Commute, SemiconjBy] using hp
simp only [this]
convert (Commute.op h).mul_geom_sum₂_Ico hmn
