00.03.01 · precalc / equations-lines

Linear equations and the line

shipped3 tiersLean: partial

Anchor (Master): Descartes 1637 La Géométrie; Cramer 1750 Introduction à l'analyse des lignes courbes algébriques; Klein 1872 Erlangen Programm; Lang Linear Algebra Ch. I; Audin Geometry Ch. I

Intuition [Beginner]

A linear equation in two variables $x$ and $y$ is an equation that can be written in the form $a x + b y = c$ , where $a$ , $b$ , $c$ are numbers and $a$ , $b$ are not both zero. The set of points $(x, y)$ in the plane that satisfy the equation is a straight line. Every line in the plane is the solution set of some linear equation, and the correspondence runs both ways.

The most familiar form is slope-intercept form, $y = m x + b$ . The number $m$ is the slope — how steeply the line rises as you move to the right — measured as rise over run. The number $b$ is the y-intercept, the height at which the line crosses the vertical axis. Once you know $m$ and $b$ , you can draw the line: mark $(0, b)$ on the vertical axis, then step right by $1$ and up by $m$ to reach the next point.

Two lines in the plane behave in one of three ways. They cross at exactly one point if their slopes differ. They never meet if they have the same slope but different intercepts (parallel lines). They lie on top of each other if they have the same slope and the same intercept (the same line). The slope is the single number that decides which of the three holds.

Visual [Beginner]

Picture two lines drawn on a coordinate grid. The first is $y = (1/2) x + 1$ , rising gently from the left, crossing the vertical axis at height $1$ , and continuing upward to the right. The second is $y = - x + 4$ , descending from the upper left, crossing the first line at the point $(2, 2)$ , and continuing down past the horizontal axis. The intersection point is marked with a dot, and both axes are labelled.

The picture records the central fact. Each line is the solution set of one linear equation, and the intersection of the two lines is the simultaneous solution of the two equations. When two lines have different slopes, they meet at exactly one point. When the slopes match, they either never meet (parallel) or coincide everywhere (the same line). Reading the slope off the picture is the first thing to do when reasoning about a system of two linear equations.

Worked example [Beginner]

Take the equation $2 x + 3 y = 6$ and put it into slope-intercept form. Subtract $2 x$ from both sides to get $3 y = - 2 x + 6$ , then divide by $3$ to get $y = - \frac{2}{3} x + 2$ . The slope is $- \frac{2}{3}$ and the y-intercept is $2$ . The line crosses the vertical axis at $(0, 2)$ . To find where it crosses the horizontal axis, set $y = 0$ : $- \frac{2}{3} x + 2 = 0$ , so $x = 3$ . The line passes through $(0, 2)$ and $(3, 0)$ .

Now solve the two-equation system $2 x + y = 5$ and $x - y = 1$ . Add the two equations side by side: the $y$ terms cancel, leaving $3 x = 6$ , so $x = 2$ . Substitute back into the second equation: $2 - y = 1$ , so $y = 1$ . The unique intersection point is $(2, 1)$ . Check by plugging into the first equation: $2 \cdot 2 + 1 = 5$ , correct.

What this tells us: a linear equation in two variables is the same algebraic object as a line in the plane, and a system of two such equations asks for the meeting point of two lines. The arithmetic of solving the system matches the geometry of finding where the lines cross.

Check your understanding [Beginner]

Formal definition [Intermediate+]

A linear equation in $n$ variables over a field $k$ is an equation of the form

a_{1} x_{1} + a_{2} x_{2} + \dots + a_{n} x_{n} = b,

with coefficients $a_{1}, \dots, a_{n}, b \in k$ and the $a_{i}$ not all zero ^{[Lang — Basic Mathematics Ch. 3–4]}. A solution is a tuple $(x_{1}, \dots, x_{n}) \in k^{n}$ satisfying the equation. The solution set is a hyperplane in $k^{n}$ : a codimension- $1$ affine subspace.

For $n = 2$ over $k = R$ , the solution set of $a x + b y = c$ with $(a, b) \neq = (0, 0)$ is a line in $R^{2}$ . Two equivalent presentations describe the same line. The implicit form is the equation $a x + b y = c$ itself. The parametric form is ${p_{0} + t v : t \in R}$ , where $p_{0} \in R^{2}$ is any solution and $v \in R^{2} ∖ {0}$ is a direction vector satisfying $a v_{1} + b v_{2} = 0$ . The vector $(a, b)$ is the normal to the line, since the implicit equation expresses orthogonality to $(a, b)$ after translation by $p_{0}$ .

When $b \neq = 0$ the implicit form rearranges to slope-intercept form $y = m x + c^{'}$ with $m = - a / b$ the slope and $c^{'} = c / b$ the y-intercept. The vertical line $x = c / a$ (with $b = 0$ ) has no slope-intercept form; its slope is undefined. Two non-vertical lines are parallel iff they share the same slope, and perpendicular iff the product of their slopes is $- 1$ . The product-equals- $- 1$ criterion follows from the fact that the direction vectors of perpendicular lines satisfy $v \cdot w = 0$ , and the slope of a line with direction vector $v = (v_{1}, v_{2})$ is $v_{2} / v_{1}$ .

Counterexamples to common slips

A linear equation in two variables is not a function $y = f (x)$ in general. The vertical line $x = 3$ has no slope-intercept form because solving for $y$ in $0 \cdot y = c$ either has every $y$ as a solution or none. The implicit form $a x + b y = c$ covers every line, including the vertical ones.
"Parallel" requires distinct lines. Two identical lines $a_{1} x + b_{1} y = c_{1}$ and $a_{2} x + b_{2} y = c_{2}$ are not parallel in the geometric sense — they coincide. The classification by the determinant $a_{1} b_{2} - a_{2} b_{1}$ (below) handles both parallel and coincident lines as the case $D = 0$ , with the relative proportionality of $c_{1}, c_{2}$ distinguishing them.
The slope-perpendicularity rule $m_{1} m_{2} = - 1$ assumes both lines are non-vertical. A vertical line is perpendicular to every horizontal line ( $m = 0$ ), but the product $m_{1} \cdot undefined$ is not $- 1$ in any algebraic sense. The product criterion is a corollary of the vector dot-product criterion, which works uniformly for all lines.

Key theorem with proof [Intermediate+]

Theorem (classification of two-line intersections). Let $L_{1}$ and $L_{2}$ be the lines in $R^{2}$ defined by the linear equations

a_{1} x + b_{1} y = c_{1}, a_{2} x + b_{2} y = c_{2},

with $(a_{i}, b_{i}) \neq = (0, 0)$ for $i = 1, 2$ . Let

D := a_{1} b_{2} - a_{2} b_{1} .

Then exactly one of the following holds.

(a) If $D \neq = 0$ , the system has a unique solution, given by Cramer's rule: $$ x = \frac{c_1 b_2 - c_2 b_1}{D}, \qquad y = \frac{a_1 c_2 - a_2 c_1}{D}. $$ The two lines meet in exactly one point.

(b) If $D = 0$ and $(a_{1}, b_{1}, c_{1})$ , $(a_{2}, b_{2}, c_{2})$ are proportional (there exists $λ \neq = 0$ with $(a_{2}, b_{2}, c_{2}) = λ (a_{1}, b_{1}, c_{1})$ ), the two equations define the same line. The two lines coincide and have infinitely many common points.

Proof. Case $D \neq = 0$ . The coefficient matrix $A = (a_{1} a_{2} b_{1} b_{2})$ has determinant $D$ , hence is invertible with inverse $A^{- 1} = \frac{1}{D} (b_{2} - a_{2} - b_{1} a_{1})$ . Solving $A (y x) = (c _{2} c _{1})$ gives

(y x) = A^{- 1} (c _{2} c _{1}) = \frac{1}{D} (a _{1} c _{2} - a _{2} c _{1} c _{1} b _{2} - c _{2} b _{1}) .

Substituting back verifies that this pair satisfies both equations. Uniqueness is automatic from invertibility of $A$ .

Case $D = 0$ , proportional triples. Write $(a_{2}, b_{2}, c_{2}) = λ (a_{1}, b_{1}, c_{1})$ with $λ \neq = 0$ . The second equation $a_{2} x + b_{2} y = c_{2}$ is then $λ (a_{1} x + b_{1} y) = λ c_{1}$ , equivalent to the first after dividing by $λ$ . Every solution of the first is a solution of the second and vice versa, so the two lines coincide.

Case $D = 0$ , non-proportional triples. Suppose for contradiction that the two lines share a common point $(x_{0}, y_{0})$ . Then $a_{1} x_{0} + b_{1} y_{0} = c_{1}$ and $a_{2} x_{0} + b_{2} y_{0} = c_{2}$ . The condition $D = 0$ means $a_{1} b_{2} = a_{2} b_{1}$ , so the vectors $(a_{1}, b_{1})$ and $(a_{2}, b_{2})$ are proportional in $R^{2}$ . Pick $μ \in R$ with $(a_{2}, b_{2}) = μ (a_{1}, b_{1})$ . (This $μ$ is unique because $(a_{1}, b_{1}) \neq = 0$ ; if $b_{1} = 0$ then $a_{1} \neq = 0$ and the proportionality is read off the first coordinate, and similarly otherwise.) Evaluating: $c_{2} = a_{2} x_{0} + b_{2} y_{0} = μ (a_{1} x_{0} + b_{1} y_{0}) = μ c_{1}$ . Then $(a_{2}, b_{2}, c_{2}) = μ (a_{1}, b_{1}, c_{1})$ , contradicting the non-proportionality hypothesis. So the two lines share no common point. $□$

Bridge. The classification of two-line intersections builds toward the general theory of linear systems and the algebraic-geometric correspondence that organises every later use of "line" in the curriculum. First, the determinant $D = a_{1} b_{2} - a_{2} b_{1}$ is the simplest nonzero example of the determinant introduced in 01.01.07 as the obstruction to invertibility of a matrix; the $2 \times 2$ case is the first place this obstruction appears, and Cramer's rule for the $2 \times 2$ system is the prototype of Cramer's rule for $n \times n$ systems with the $n$ -by- $n$ determinant in the denominator. Second, the matrix equation $A (y x) = (c _{2} c _{1})$ is the simplest instance of the abstract setup $T (v) = w$ for a linear map $T : V \to W$ between vector spaces, the central object of linear algebra in [01.01.*]: the unique-solution case corresponds to $T$ an isomorphism, the no-solution case to $w \in / im (T)$ , and the infinitely-many-solutions case to $dim ker (T) > 0$ . Third, the parametric form $p_{0} + t v$ is the prototype of an affine subspace — a translate $p_{0} + W$ of a linear subspace $W$ — and the distinction between affine and linear (lines through the origin are linear, general lines are affine) is the first appearance of a distinction that runs through every later geometry unit.

Putting these together, the linear equation in two variables is the foundational object whose algebra generalises in three coordinated directions. The determinant generalises from the $2 \times 2$ scalar $a_{1} b_{2} - a_{2} b_{1}$ to the $n \times n$ alternating multilinear form, reappearing as the Jacobian determinant in the multivariable change-of-variables formula and as the obstruction to invertibility in every linear map between equal-dimension spaces. The line generalises from a one-dimensional affine subspace of $R^{2}$ to the affine flats of $R^{n}$ (codimension- $k$ flats are solution sets of $k$ independent linear equations) and then to the hyperplanes and lines of projective space $P^{n}$ . The system generalises from two equations in two unknowns to Gaussian elimination on an $m \times n$ system, the entire theory of rank, kernel, image, and rank-nullity. The line is the foundational geometric object whose algebra is the seed of all of linear algebra, and the classification proved above is the seed of the entire structure theory of linear systems.

Exercises [Intermediate+]

Exercise 5 (medium, symbolic).

Show that the line $L : a x + b y = c$ in $R^{2}$ with $(a, b) \neq = (0, 0)$ admits the parametric description $L = {p_{0} + t v : t \in R}$ , where $p_{0}$ is any point on $L$ and $v = (- b, a)$ .

Hint

Verify that $p_{0} + t v$ satisfies the equation for every $t$ , and that every solution has this form.

Answer

Write $p_{0} = (x_{0}, y_{0})$ with $a x_{0} + b y_{0} = c$ . For $p_{0} + t v = (x_{0} - t b, y_{0} + t a)$ , the equation evaluates to $a (x_{0} - t b) + b (y_{0} + t a) = a x_{0} + b y_{0} - t ab + t ba = c$ , so every $p_{0} + t v$ lies on $L$ . Conversely, if $(x, y)$ lies on $L$ , the difference $(x - x_{0}, y - y_{0})$ satisfies $a (x - x_{0}) + b (y - y_{0}) = 0$ . Since $(a, b) \neq = 0$ , the vector $(x - x_{0}, y - y_{0})$ is a scalar multiple of any nonzero vector orthogonal to $(a, b)$ . The vector $(- b, a)$ is such a vector (the dot product $a \cdot (- b) + b \cdot a = 0$ ), so there exists $t$ with $(x - x_{0}, y - y_{0}) = t (- b, a)$ , that is, $(x, y) = p_{0} + t v$ .

Rubric: full credit for both directions of the equivalence — verifying that the parametric form satisfies the equation, and showing every solution is of the parametric form via the orthogonal-direction argument.

Exercise 6 (hard, symbolic).

Three lines $L_{1} : a_{1} x + b_{1} y = c_{1}$ , $L_{2} : a_{2} x + b_{2} y = c_{2}$ , $L_{3} : a_{3} x + b_{3} y = c_{3}$ in $R^{2}$ are said to be concurrent if there is a single point lying on all three. Show that if $L_{1}$ and $L_{2}$ meet at a unique point (so $a_{1} b_{2} - a_{2} b_{1} \neq = 0$ ), then $L_{1}, L_{2}, L_{3}$ are concurrent iff the $3 \times 3$ determinant

det a_{1} a_{2} a_{3} b_{1} b_{2} b_{3} c_{1} c_{2} c_{3} = 0.

Hint

Compute the intersection point of $L_{1}$ and $L_{2}$ by Cramer's rule, then express the condition that this point lies on $L_{3}$ in determinant form by expanding the $3 \times 3$ determinant along the bottom row.

Answer

By the theorem, the unique intersection of $L_{1}$ and $L_{2}$ is $(x_{0}, y_{0})$ with $x_{0} = (c_{1} b_{2} - c_{2} b_{1}) / D$ and $y_{0} = (a_{1} c_{2} - a_{2} c_{1}) / D$ , where $D = a_{1} b_{2} - a_{2} b_{1}$ . The three lines are concurrent iff $(x_{0}, y_{0})$ lies on $L_{3}$ , that is, $a_{3} x_{0} + b_{3} y_{0} - c_{3} = 0$ . Multiplying through by $D$ , this is equivalent to $a_{3} (c_{1} b_{2} - c_{2} b_{1}) + b_{3} (a_{1} c_{2} - a_{2} c_{1}) - c_{3} (a_{1} b_{2} - a_{2} b_{1}) = 0$ . The left-hand side is the expansion of the $3 \times 3$ determinant in the statement along the bottom row, multiplied by $- 1$ . Hence the determinant vanishes iff the three lines are concurrent.

Rubric: full credit for computing the intersection via Cramer's rule, substituting into the third equation, and identifying the resulting expression as the cofactor expansion of the $3 \times 3$ determinant.

Exercise 7 (hard, short-answer).

Let $L$ be a line in $R^{2}$ given by $a x + b y = c$ with $(a, b) \neq = (0, 0)$ . Show that the perpendicular distance from a point $P = (x_{0}, y_{0})$ to $L$ is given by

d (P, L) = \frac{∣ a x _{0} + b y _{0} - c ∣}{a ^{2} + b ^{2}} .

Hint

The vector $(a, b)$ is normal to $L$ . Drop a perpendicular from $P$ to $L$ in the direction of the unit normal $(a, b) / a^{2} + b^{2}$ .

Answer

Let $Q = (x_{1}, y_{1})$ be the foot of the perpendicular from $P$ to $L$ . Then $Q$ lies on $L$ , so $a x_{1} + b y_{1} = c$ . The displacement $P - Q$ is a scalar multiple of the normal $(a, b)$ : write $P - Q = t (a, b)$ for some $t \in R$ . Then $P = Q + t (a, b)$ , so $a x_{0} + b y_{0} = a (x_{1} + t a) + b (y_{1} + t b) = c + t (a^{2} + b^{2})$ , giving $t = (a x_{0} + b y_{0} - c) / (a^{2} + b^{2})$ . The distance is $∣ P - Q ∣ = ∣ t ∣ a^{2} + b^{2} = ∣ a x_{0} + b y_{0} - c ∣/ a^{2} + b^{2}$ .

Rubric: full credit for setting up the perpendicular along the normal direction, solving for the parameter $t$ , and computing the resulting distance.

Lean formalization [Intermediate+]

[object Promise]

The four named statements compile against Mathlib's Matrix infrastructure. The proofs are deferred — Mathlib supplies Matrix.det_fin_two for the two-by-two determinant, Matrix.cramer for the unique-solution formula when the determinant is a unit, and AffineSubspace.mk' for the affine-subspace structure on the solution set of a single linear equation. The human reviewer named in the frontmatter signs off on the coverage claim.

Advanced results [Master]

The classification of two-line intersections is the prototype of the structure theory of linear systems, and the generalisations follow in three coordinated directions: dimension, base field, and the affine-versus-linear distinction.

Linear versus affine. A linear subspace of $R^{n}$ is a subset $W$ closed under addition and scalar multiplication, equivalently the kernel of a linear map or the solution set of a homogeneous linear system $A x = 0$ . An affine subspace is a translate $p_{0} + W$ of a linear subspace, equivalently the solution set of a possibly inhomogeneous system $A x = b$ for some $b \in im (A)$ ^{[Audin — Geometry Ch. I]}. A line through the origin is a one-dimensional linear subspace; a general line is a one-dimensional affine subspace. The set of affine subspaces of $R^{n}$ of a given dimension forms a homogeneous space under the affine group $Aff (R^{n}) = R^{n} ⋊ GL (n, R)$ , the semidirect product of translations with the general linear group. The distinction between the two becomes structural in the differential-geometric setting: a tangent space at a point is a linear subspace, while a tangent affine subspace (the actual tangent line, plane, etc., physically located at the point) is its affine translate.

Hyperplanes and flats. A hyperplane in $R^{n}$ is a codimension- $1$ affine subspace, the solution set of a single linear equation $a_{1} x_{1} + \dots + a_{n} x_{n} = b$ with $(a_{1}, \dots, a_{n}) \neq = 0$ . A general flat of codimension $k$ is the intersection of $k$ hyperplanes whose normal vectors are linearly independent, equivalently the solution set of a system $A x = b$ where $A$ is $k \times n$ of rank $k$ . The classification of two-line intersections generalises to the Frobenius / Kronecker-Capelli theorem: a linear system $A x = b$ is consistent iff $rank (A) = rank ([A ∣ b])$ , and the solution set, when nonempty, is an affine subspace of dimension $n - rank (A)$ . The unique-solution case ( $A$ invertible) recovers Cramer's rule, the no-solution case corresponds to $b \in / im (A)$ , and the infinitely-many-solutions case corresponds to $dim ker (A) > 0$ .

Cramer's rule in general. For a square system $A x = b$ with $A \in Mat_{n \times n} (k)$ and $det A \neq = 0$ , the unique solution has $i$ -th component

x_{i} = \frac{det A _{i}}{det A},

where $A_{i}$ is the matrix obtained from $A$ by replacing the $i$ -th column with $b$ ^{[Cramer — Introduction à l'analyse des lignes courbes algébriques]}. The $2 \times 2$ case of the theorem above is the instance $n = 2$ . Cramer's rule is rarely used computationally for large $n$ (Gaussian elimination scales as $O (n^{3})$ while expansion of an $n \times n$ determinant scales as $O (n!)$ ), but it remains structurally important: it expresses each component of the solution as a ratio of determinants, making the algebraic dependence on the matrix entries explicit and supplying the determinant identity behind the adjugate-inverse formula $A^{- 1} = adj (A) / det A$ .

Projective lines. The projective line over $R$ is $P^{1} (R) = (R^{2} ∖ {0}) / \sim$ , where $(x, y) \sim (λ x, λ y)$ for $λ \neq = 0$ . As a set, $P^{1} (R) = R \cup {\infty}$ : the equivalence class of $(x, y)$ with $y \neq = 0$ is identified with $x / y \in R$ , and the class of $(x, 0)$ is the point at infinity. The projective line is the natural ambient space for projective geometry — Klein's 1872 Erlangen Programm placed the geometry of $P^{1}$ as the symmetry under the projective linear group $PGL (2, R)$ , acting by Möbius transformations $z \mapsto (a z + b) / (cz + d)$ with $a d - b c \neq = 0$ ^{[Klein — Vergleichende Betrachtungen über neuere geometrische Forschungen]}. Three distinct points of $P^{1}$ form a frame: any three points map to any other three by a unique Möbius transformation, and the canonical reference frame is ${0, 1, \infty}$ . The projective line over $C$ is the Riemann sphere $P^{1} (C) = C \cup {\infty}$ , central to complex analysis.

Linear codes. In coding theory, a linear code over $F_{q}$ of block length $n$ and dimension $k$ is a $k$ -dimensional linear subspace $C \subseteq F_{q}^{n}$ . The code is the kernel of a parity-check matrix $H \in Mat_{(n - k) \times n} (F_{q})$ , equivalently the image of a generator matrix $G \in Mat_{k \times n} (F_{q})$ . The minimum-distance and rate-versus-distance trade-off of a linear code (the Singleton bound $d \leq n - k + 1$ , achieved by MDS codes such as Reed-Solomon) is the central problem of algebraic coding theory. The geometric content: a linear code is a finite-field analogue of a linear subspace of $R^{n}$ , and the codewords are the lattice points of that subspace.

Convex polytopes and half-spaces. A half-space in $R^{n}$ is the solution set of a linear inequality $a_{1} x_{1} + \dots + a_{n} x_{n} \leq b$ . A convex polytope is a bounded intersection of finitely many half-spaces. The structure theory of polytopes — vertices, edges, faces, the face lattice, the $f$ -vector — sits on top of the linear-equation foundation: each face of a polytope is the intersection of the polytope with a hyperplane that touches it at the face and bounds it on one side. The duality between vertex description ( $V$ -polytope) and half-space description ( $H$ -polytope), proved by Minkowski-Weyl, is the polytopal generalisation of the implicit-versus-parametric duality of a single linear equation.

Synthesis. The bridge between the elementary classification of two-line intersections and the broader theory of linear systems is the recognition that the determinant $D = a_{1} b_{2} - a_{2} b_{1}$ is the single load-bearing invariant — once the determinant has been identified as the obstruction to invertibility, the unique-solution case, the parallel case, and the coincident case all read off as the three possibilities for the rank of the coefficient matrix. The $2 \times 2$ determinant generalises to the $n \times n$ determinant, the classification to the Frobenius / Kronecker-Capelli theorem, the line to the hyperplane and the affine flat, and Cramer's rule to the general $n$ -by- $n$ solution formula. This is precisely the structural content the algebra strand reads off in 01.01.07: the determinant is the obstruction to invertibility, the rank measures the dimension of the image, and the solution geometry of a linear system is governed by exactly two integer invariants, $rank (A)$ and $rank ([A ∣ b])$ .

The same machinery extends to projective geometry, where the line is replaced by the projective subspace and the affine group by the projective linear group. Klein's Erlangen Programm organised the resulting hierarchy: affine geometry studies invariants under $Aff (R^{n})$ , projective geometry under $PGL (n + 1)$ , Euclidean under $O (n) ⋉ R^{n}$ , and each lower geometry's invariants are a special case of the higher one's. The line is the foundational geometric object whose algebra is the seed of all of linear algebra, and whose generalisations are the entry points to affine geometry, projective geometry, convex geometry, and algebraic coding theory. Putting these together, the foundational insight is that a linear equation in $n$ variables is the abstract presentation of a hyperplane, the solution set of a system is the intersection of hyperplanes, and the structure theory of linear systems is the algebraic shadow of the geometry of flats in affine and projective space. This unit identifies the line as the prototype hyperplane, identifies the $2 \times 2$ determinant as the obstruction to unique intersection, identifies the parametric form as the affine version of a linear subspace, and identifies the projective line as the natural completion of the affine line.

Full proof set [Master]

Proposition (Cramer's rule, $n \times n$ case). Let $A \in Mat_{n \times n} (k)$ with $det A \neq = 0$ and $b \in k^{n}$ . The unique solution of $A x = b$ has components $x_{i} = det A_{i} / det A$ , where $A_{i}$ is $A$ with its $i$ -th column replaced by $b$ .

Proof. Since $det A \neq = 0$ , $A$ is invertible with $A^{- 1} = adj (A) / det A$ , where the $(i, j)$ entry of $adj (A)$ is the $(j, i)$ cofactor of $A$ . Then $x = A^{- 1} b$ has $i$ -th component $x_{i} = \sum_{j} (adj (A))_{ij} b_{j} / det A = \sum_{j} (- 1)^{i + j} M_{j i} b_{j} / det A$ , where $M_{j i}$ is the minor obtained by deleting row $j$ and column $i$ of $A$ . The numerator is the cofactor expansion of $det A_{i}$ along the $i$ -th column (which contains the entries $b_{1}, \dots, b_{n}$ ). Hence $x_{i} = det A_{i} / det A$ .

Proposition (Frobenius / Kronecker-Capelli). A linear system $A x = b$ with $A \in Mat_{m \times n} (k)$ , $b \in k^{m}$ has a solution iff $rank (A) = rank ([A ∣ b])$ , where $[A ∣ b]$ is the augmented matrix. When nonempty, the solution set is an affine subspace of $k^{n}$ of dimension $n - rank (A)$ .

Proof. The system has a solution iff $b \in im (A) = col (A)$ , the column space of $A$ . The column space of $[A ∣ b]$ is spanned by the columns of $A$ together with $b$ , so $rank ([A ∣ b]) = rank (A)$ iff $b \in col (A)$ . When the system is consistent, the solution set is the preimage $A^{- 1} ({b})$ . Fix any particular solution $x_{0}$ . Then $x \in A^{- 1} ({b})$ iff $A (x - x_{0}) = 0$ , that is, $x - x_{0} \in ker (A)$ . So the solution set is the affine subspace $x_{0} + ker (A)$ . The rank-nullity theorem $dim ker (A) + rank (A) = n$ gives $dim ker (A) = n - rank (A)$ .

Proposition (transitive action of Möbius transformations). The group $PGL (2, R)$ acts on $P^{1} (R)$ by $[A] \cdot [v] = [A v]$ , and the action is sharply $3$ -transitive: for any two ordered triples $(p_{1}, p_{2}, p_{3})$ and $(q_{1}, q_{2}, q_{3})$ of distinct points of $P^{1} (R)$ , there is a unique element of $PGL (2, R)$ sending $p_{i}$ to $q_{i}$ for $i = 1, 2, 3$ .

Proof sketch. Existence: it suffices to show every triple of distinct points can be sent to the canonical frame $(0, 1, \infty)$ by an element of $PGL (2, R)$ , then compose. The Möbius transformation $z \mapsto (z - p_{1}) / (z - p_{3}) \cdot (p_{2} - p_{3}) / (p_{2} - p_{1})$ sends $p_{1} \mapsto 0$ , $p_{2} \mapsto 1$ , $p_{3} \mapsto \infty$ (with appropriate limit interpretation if any $p_{i} = \infty$ ). Uniqueness: a Möbius transformation fixing three distinct points is the identity. If $z \mapsto (a z + b) / (cz + d)$ fixes $0, 1, \infty$ , then fixing $\infty$ gives $c = 0$ , fixing $0$ gives $b = 0$ , fixing $1$ gives $a = d$ , so the matrix is a nonzero scalar multiple of the identity and represents the identity in $PGL (2, R)$ .

Proposition (Minkowski-Weyl, statement). A subset $P \subseteq R^{n}$ is a bounded intersection of finitely many half-spaces (an $H$ -polytope) iff it is the convex hull of finitely many points (a $V$ -polytope).

Proof. Stated without proof; see Ziegler Lectures on Polytopes Ch. 1 for the standard development via Fourier-Motzkin elimination, the linear-programming duality theorem, and Carathéodory's theorem. The bridge from the linear-equation foundation here is that each facet (codimension- $1$ face) of a polytope corresponds to one of the defining linear inequalities turning into a tight linear equation, so the face lattice of a polytope is the combinatorial shadow of a finite collection of linear equations and inequalities.

Connections [Master]

The two-by-two determinant $D = a_{1} b_{2} - a_{2} b_{1}$ proved here as the obstruction to unique intersection is the simplest nonzero instance of the general determinant introduced in 01.01.07. Cramer's rule for the $2 \times 2$ system is the prototype of Cramer's rule for the $n \times n$ system, and the classification of two-line intersections is the prototype of the Frobenius / Kronecker-Capelli theorem governing arbitrary linear systems. The determinant reappears throughout the curriculum: as the Jacobian determinant in multivariable change of variables in 02.05.04, as the obstruction to local invertibility of a smooth map at a point, and as the top exterior power of a linear endomorphism in 01.01.10 pending.
The matrix equation $A (y x) = (c _{2} c _{1})$ studied here is the simplest instance of the abstract setup $T (v) = w$ for a linear map $T : V \to W$ between vector spaces, the central object of linear algebra in 01.01.03 (vector space) and 01.01.06 pending (linear transformation, kernel, image, rank-nullity). The three cases of the classification — unique solution, no solution, infinitely many solutions — correspond exactly to the three structural possibilities for a linear map between equal-dimension spaces: isomorphism, inconsistency ( $w \in / im (T)$ ), and nontrivial kernel. The line itself is the simplest example of an affine subspace, the geometric setting where vectors are points rather than displacements.
The projective line $P^{1} (R) = R \cup {\infty}$ and the action of $PGL (2, R)$ by Möbius transformations introduced in the Advanced results section reappear in 06.01.07 (Riemann sphere) and 06.01.08 (Möbius transformations) as the central organising structures of complex analysis on $P^{1} (C)$ . The same group-theoretic content — three distinct points form a sharp frame — is the basis of the cross-ratio invariant of projective geometry, and the same algebra of $2 \times 2$ matrices acting on the projective line drives the spectral theory of Schwarzian derivatives and one-dimensional projective structures.
The affine-versus-linear distinction sharpened here recurs throughout differential geometry. A tangent space at a point of a manifold is a linear subspace of the ambient vector space, while the tangent affine subspace (the actual tangent line, plane, etc.) is its affine translate located at the point. This distinction is the source of the affine-vs-linear gap in the formulation of geodesics, in the affine connections of 03.02.01, and in the principal-bundle reformulation of gauge theory where the affine action of a structure group on a fibre is the load-bearing operation.

Historical & philosophical context [Master]

The geometric line predates the algebraic line by more than two millennia. Euclid's Elements (~300 BCE) Book I opens with the postulates of plane geometry, taking the line as a primitive object characterised by axioms: through any two distinct points there is exactly one line, any line can be extended indefinitely, and through any point not on a given line there is exactly one line parallel to it (the parallel postulate). The Euclidean line is a synthetic object with no algebraic description. René Descartes, in his 1637 La Géométrie (an appendix to the Discours de la méthode), introduced the correspondence between algebraic equations and geometric loci that organises every modern treatment of the line: a curve in the plane is the solution set of an equation $f (x, y) = 0$ , and the simplest non-degenerate case is the linear equation $a x + b y = c$ , whose solution set is a straight line ^{[Descartes — La Géométrie]}. Pierre de Fermat, in unpublished manuscripts circulating from 1636, independently introduced the same algebraic-geometric correspondence; his Ad locos planos et solidos isagoge (composed ~1636, published posthumously in 1679) gave the equation of a straight line in essentially modern form.

The determinant rule for solving systems of linear equations is due to Gabriel Cramer, who stated and applied it in the appendix to his 1750 Introduction à l'analyse des lignes courbes algébriques ^{[Cramer — Introduction à l'analyse des lignes courbes algébriques]}. Cramer derived the rule for $n \times n$ systems by extrapolating from the small- $n$ cases without explicit recursive structure; the modern cofactor-expansion development of the determinant came later, with Pierre-Simon Laplace (1772), Augustin-Louis Cauchy (1812), and Carl Gustav Jacob Jacobi (1841) supplying the systematic theory. Felix Klein, in his 1872 inaugural lecture at Erlangen, organised geometry by symmetry groups: the projective line $P^{1}$ with its $PGL (2)$ symmetry sits at the top of a hierarchy whose lower floors are affine geometry, similarity geometry, and Euclidean geometry, each obtained by restricting the symmetry group ^{[Klein — Vergleichende Betrachtungen über neuere geometrische Forschungen]}. The line, in each of these geometries, is the canonical one-dimensional flat: a line through the origin in linear algebra, an affine line in affine geometry, a projective line in projective geometry.

Bibliography [Master]

[object Promise]

Prerequisites

00.01.01

Tier anchors

beginner: Lang Basic Mathematics Ch. 3; Strogatz-style line-on-the-plane picture
intermediate: Lang Basic Mathematics Ch. 3–4; Apostol Vol. 1 §3.1; Lay Linear Algebra Ch. 1.1–1.2
master: Descartes 1637 La Géométrie; Cramer 1750 Introduction à l'analyse des lignes courbes algébriques; Klein 1872 Erlangen Programm; Lang Linear Algebra Ch. I; Audin Geometry Ch. I

References

TODO_REF
Lang — Basic Mathematics · Ch. 3–4, linear equations and the line
TODO_REF
Apostol — Calculus Vol. 1 · §3.1, equations of lines
TODO_REF
Lay — Linear Algebra and Its Applications · Ch. 1.1–1.2, systems of linear equations
TODO_REF
Descartes — La Géométrie · 1637, Books I–II, coordinate geometry
TODO_REF
Cramer — Introduction à l'analyse des lignes courbes algébriques · 1750, Appendix I, determinant rule
TODO_REF
Klein — Vergleichende Betrachtungen über neuere geometrische Forschungen · Erlangen 1872, projective hierarchy
TODO_REF
Audin — Geometry · Ch. I, affine geometry and lines

Lean module

Codex.Precalc.Equations.LinesPlane

Mathlib gap

Mathlib supplies Matrix and Matrix.det for square matrices over a commutative ring, the two-by-two determinant via Matrix.det_fin_two, the Module instance on Fin n → K for K a field, and AffineSubspace.mk' with the affineSpan construction for affine subspaces of a vector space. Cramer's rule is packaged in Mathlib.LinearAlgebra.Matrix.Cramer as Matrix.cramer applied to the coefficient matrix, and Matrix.mulVec_cramer assembles the unique solution when the determinant is a unit. What is not packaged as a single named lemma is the textbook classification of two-line systems in the plane into the three cases parallel, coincident, and unique intersection, indexed by the sign of the two-by-two determinant; the companion module states the four signature results and defers the proofs while the human reviewer signs off on the coverage claim.

Reviewer

TBD

Estimated time

beginner: 14m
intermediate: 30m
master: 50m