geom_sum_eq_zero_iff_neg_one — Mathlib

English

The geometric sum equals zero exactly when x = -1 and n is even (with n ≠ 0).

Русский

Геометрическая сумма равна нулю тогда и только тогда, когда x = −1 и n чётно (n ≠ 0).

LaTeX

$$$n \\neq 0 \\Rightarrow \\sum_{i=0}^{n-1} x^i = 0 \\iff x = -1 \\land \\text{Even}(n)$$$

Lean4

theorem geom_sum_eq_zero_iff_neg_one (hn : n ≠ 0) : ∑ i ∈ range n, x ^ i = 0 ↔ x = -1 ∧ Even n :=
  by
  refine ⟨fun h => ?_, @fun ⟨h, hn⟩ => by simp only [h, hn, neg_one_geom_sum, if_true]⟩
  contrapose! h
  have hx := eq_or_ne x (-1)
  rcases hx with hx | hx
  · rw [hx, neg_one_geom_sum]
    simp only [h hx, ite_false, ne_eq, one_ne_zero, not_false_eq_true]
  · exact geom_sum_ne_zero hx hn

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