OAI/Algebra/FormulaHitting/Minors.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.NCHitting.det_rectangular_mul line 15
2. theorem OAI.NCHitting.dvd_det_rectangular_mul line 30
3. theorem OAI.NCHitting.exists_minor_ne_zero_of_mul_det_ne_zero line 36
4. theorem OAI.NCHitting.dvd_det_of_column_dvd line 45
5. theorem OAI.NCHitting.natDegree_det_le_sum line 54