General = particular + homogeneous

Proved

HefferonLinAlg.general_eq_particular_plus_homogeneous

by tianyipeng · Aug 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

affine-subspacelinear-algebralinear-systems

Let $A$ be an $m \times n$ matrix over a field $K$ , let $b \in K^m$ , and suppose $p \in K^n$ is one particular solution, $Ap = b$ . Then the solution set of $Ax = b$ is exactly $\{\, p + h : Ah = 0 \,\}$ . Every solution is the particular solution plus a solution of the associated homogeneous system, and conversely every such sum solves the system. This is the structural description of a solution set that Hefferon returns to throughout the book.

Preamble

import Mathlib

open Matrix

Formal statement

namespace HefferonLinAlg

theorem general_eq_particular_plus_homogeneous
    {K : Type*} [Field K] {m n : ℕ}
    (A : Matrix (Fin m) (Fin n) K) (b : Fin m → K) (p : Fin n → K) (hp : A *ᵥ p = b) :
    {x : Fin n → K | A *ᵥ x = b} = {x : Fin n → K | ∃ h, A *ᵥ h = 0 ∧ x = p + h} := by
  sorry

end HefferonLinAlg

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter One, Section I.3, Theorem 3.1, p. 33

Read-back

What the Lean code literally says, in plain math · claude-opus-5

The declaration HefferonLinAlg.general_eq_particular_plus_homogeneous asserts the following. Let $K$ be an arbitrary type carrying a field structure (in particular $0 \neq 1$ ; no assumption of finiteness, of characteristic, or of algebraic closure is made), and let $m, n$ be arbitrary natural numbers — both are implicit and unconstrained, so the statement includes the degenerate cases $m = 0$ (a matrix with no rows) and $n = 0$ (a matrix with no columns, where $K^{n}$ is the one-point space consisting of the empty vector). Let

$A \in K^{m \times n}$ be a matrix whose rows are indexed by $\{0, \dots, m-1\}$ and whose columns are indexed by $\{0, \dots, n-1\}$ ,
$b \in K^{m}$ be a vector (a function from the row index set to $K$ ),
$p \in K^{n}$ be a vector (a function from the column index set to $K$ ),

and assume the single hypothesis that $p$ satisfies the system, i.e.

A p = b, \qquad \text{where } (A v)_i \;=\; \sum_{j=0}^{n-1} A_{i,j}\, v_j \ \text{ for each row index } i,

this being the usual matrix–vector product, with equality of vectors meaning equality at every row index. Nothing else is assumed about $p$ : it is merely some solution, not required to be unique, nonzero, or distinguished in any way, and no assumption is made that $A$ is injective, surjective, square, or of any particular rank. Under these assumptions the theorem concludes an equality of two subsets of $K^{n}$ (equality of sets of vectors, i.e. the two sets have exactly the same members):

\{\, x \in K^{n} \;:\; A x = b \,\} \;=\; \{\, x \in K^{n} \;:\; \exists\, h \in K^{n},\ A h = 0 \ \text{ and } \ x = p + h \,\}.

Here $0$ on the right denotes the zero vector of $K^{m}$ (the function that is $0$ at every row index), the existential quantifier ranges over all vectors $h \in K^{n}$ and is a plain "there exists" with no uniqueness claim, the conjunction requires both that $h$ solve the homogeneous system and that $x$ be exactly $p + h$ , and $p + h$ denotes coordinatewise addition, $(p+h)_j = p_j + h_j$ . The claim is a full set equality (both inclusions), not one inclusion or a mere characterization up to some equivalence. In the degenerate case $m = 0$ the hypothesis $A p = b$ holds automatically (equality of two vectors with no coordinates), and both sides of the conclusion are then all of $K^{n}$ ; in the case $n = 0$ both sides are subsets of a one-element space. The statement is closed with sorry, so no proof is supplied.

Human review

Endorsed by Shuze Chen · Aug 5, 2026
Endorsed by tianyipeng · Aug 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph