op_geom_sum — Mathlib

English

The opposite-ring operation commutes with geometric sums: op(sum x^i) = sum (op x)^i.

Русский

Действие противоположной операции над геометрической суммой равно геометрической сумме применённой к противоположному элементу: op(∑ x^i) = ∑ (op x)^i.

LaTeX

$$$\\operatorname{op}\\left(\\sum_{i=0}^{n-1} x^{i}\\right) = \\sum_{i=0}^{n-1} (\\operatorname{op} x)^{i}$$$

Lean4

theorem op_geom_sum (x : R) (n : ℕ) : op (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, op x ^ i := by simp

Похожие утверждения