OAI/NumberTheory/TwoPoint/Bounds/LinearPivots.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pivot coordinates over a field

A surjective family of real linear equations has a set of pivot coordinates of the same cardinality as the equations. Fixing all other coordinates leaves at most one solution. This uses linear algebra over the original field, without reducing a determinant modulo a prime.

  1. theorem OAI.TwoPointCorrelations.exists_pivot_coordinates line 20