OAI/NumberTheory/DukePrimeDegree/Geometry/FullFrameMinors.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A nonzero coordinate minor of an independent frame

Maximal Gram minors of the row family select the required coordinate minor. Row rank equals column rank, so the selected number of rows is exactly the size of the independent column frame.

  1. theorem OAI.DukePrimeDegree.exists_nonzero_frameMinor_of_linearIndependent line 20