English
A variant of the geometric sum with opposite operations: sum i of op y^i * op x^{n-1-i} equals sum of op x^i * op y^{n-1-i}.
Русский
Вариант геометрической суммы с противоположными операциями: сумма op y^i · op x^{n-1-i} равна сумме op x^i · op y^{n-1-i}.
LaTeX
$$$\\sum_{i=0}^{n-1} \\mathrm{op}(y)^{i} \\cdot \\mathrm{op}(x)^{n-1-i} = \\sum_{i=0}^{n-1} \\mathrm{op}(y)^{n-1-i} \\cdot \\mathrm{op}(x)^{i}$$$
Lean4
@[simp]
theorem op_geom_sum₂ (x y : R) (n : ℕ) :
∑ i ∈ range n, op y ^ (n - 1 - i) * op x ^ i = ∑ i ∈ range n, op y ^ i * op x ^ (n - 1 - i) :=
by
rw [← sum_range_reflect]
refine sum_congr rfl fun j j_in => ?_
grind
