lean_workbook_plus_39783

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Find the $x_{1}, x_{2}, ..., x_{n}$ complex solutions of the following equation\n $x_{1}=\frac{1}{x_{1}}+q^{2}x_{2}=\frac{1}{x_{2}}+q^{4}x_{3}=...=\frac{1}{x_{n-1}}+q^{(n-1)2}x_{n}=\frac{1}{x_{n}}$ \nGiven: $0<q<1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39783 (n : ℕ) (q : ℝ) (hq : 0 < q ∧ q < 1) : ∃ x : ℕ → ℂ, x 1 = 1 / x 1 + q ^ 2 * x 2 ∧ x 2 = 1 / x 2 + q ^ 4 * x 3 ∧ ∀ i ∈ Finset.range n, x i = 1 / x i + q ^ (2 * i) * x (i + 1)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph