OAI/Analysis/Quantum/PPTSquare/MatrixSelection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MatrixSelection.exists_row_minor line 14
2. lemma OAI.MatrixSelection.rank_lt_of_all_row_minors_zero line 38
3. lemma OAI.MatrixSelection.all_row_minors_units line 46
4. lemma OAI.MatrixSelection.first_columns_rank line 64