lean_workbook_plus_46905

Proved

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

Let A be an $n\times m$ matrix, and $b\in \mathbb R^n$ . Suppose $Ax = b$ has at least one solution $x_0\in \mathbb R^m$ Show all solutions are of the form $x = x_0 + h$ , where $h$ solves $Ah = 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46905 {n m : ℕ} (A : Matrix (Fin n) (Fin m) ℝ) (b : Fin n → ℝ) (x0 : Fin m → ℝ) (h : A.mulVec x0 = b) : ∀ x : Fin m → ℝ, A.mulVec x = b ↔ ∃ h : Fin m → ℝ, x = x0 + h ∧ A.mulVec h = 0   :=  by sorry

Source

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

View graph