A five-equation cyclic linear system
ProvedWorkbookSource.problem_13737lean-workbooksource-checked
Find the solution for the specific system of 5 equations with RHS's = 3: , , , , .
Source: InternLM Lean-Workbook, record lean_workbook_13737 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.
Preamble
import Mathlib open Real Nat
Formal statement
theorem WorkbookSource.problem_13737 (x1 x2 x3 x4 x5 : ℝ) : x1 + x2 + x3 = 3 ∧ x2 + x3 + x4 = 3 ∧ x3 + x4 + x5 = 3 ∧ x4 + x5 + x1 = 3 ∧ x5 + x1 + x2 = 3 ↔ x1 = 1 ∧ x2 = 1 ∧ x3 = 1 ∧ x4 = 1 ∧ x5 = 1 := by sorry
Source