LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Determinant criterion: if the matrix $(⟨ v_{i}, w_{j} ⟩)_{i, j}$ is invertible then both $v_{1}, \dots, v_{m}$ and $w_{1}, \dots, w_{m}$ are linearly independent

Statement

Let $F$ be a field, let $V$ be an $F$ -vector space, and let $⟨ \cdot, \cdot ⟩ : V \times V \to F$ be a bilinear form. If the matrix

$M = (⟨ v_{i}, w_{j} ⟩)_{1 \leq i, j \leq m}$

is invertible, then both lists $v_{1}, \dots, v_{m}$ and $w_{1}, \dots, w_{m}$ are linearly independent.

Facts & Assumptions

Given: the vectors $v_{1}, \dots, v_{m}, w_{1}, \dots, w_{m}$ and the matrix $M$ above.

[F1]

Square matrices form a ring, so matrix multiplication is associative and has identity $I$ ( $M_{n} (F)$ is a ring under entrywise addition and matrix multiplication, including the zero ring $M_{0} (F)$ ). An invertible matrix $M$ has a two-sided inverse $M^{- 1}$ with $M M^{- 1} = M^{- 1} M = I$ (Invertible matrices and the general linear group ${GL}_{n} (F)$ ).

[F2]

The form is linear in each variable separately (Bilinear forms, and symmetric, skew-symmetric, and alternating bilinear forms).

Proof

technique · direct

1.1

Suppose $\sum_{i = 1}^{m} c_{i} v_{i} = 0$ . Pairing with each $w_{j}$ and using [F2] gives $\sum_{i = 1}^{m} c_{i} ⟨ v_{i}, w_{j} ⟩ = 0$ for every $j$ , which is the matrix equation $c^{T} M = 0$ .

F2assume-contra

2.1

Since $M$ is invertible, multiply on the right by $M^{- 1}$ and use [F1] to obtain $c^{T} = 0$ . So $c_{1} = \dots = c_{m} = 0$ , and the vectors $v_{1}, \dots, v_{m}$ are linearly independent.

F1step 1.1discharge-contradiction

3.1

If $\sum_{j} d_{j} w_{j} = 0$ , pairing with each $v_{i}$ and using linearity in the second variable gives $M d = 0$ . Multiplying on the left by $M^{- 1}$ and using [F1] gives $d = 0$ . Thus $w_{1}, \dots, w_{m}$ are linearly independent as well.

F1F2∎

Remarks

This is the matrix version of the diagonal and triangular criteria: there the matrix is visibly diagonal or triangular, while here only invertibility is assumed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

27 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

L. Babai and P. Frankl, Linear Algebra Methods in Combinatorics, §2.1.4 (standard reference, not scraped)

Determinant criterion: if the matrix (⟨vi,wj⟩)i,j(⟨vi​,wj​⟩)i,j​ is invertible then both v1,…,vmv1​,…,vm​ and w1,…,wmw1​,…,wm​ are linearly independent