OAI/Analysis/Quantum/DimensionTen/MinorRelations.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DimensionTen.Border.minors_eq line 10
2. lemma OAI.DimensionTen.Border.detH_ne_zero line 31
3. lemma OAI.DimensionTen.Border.H_left_inverse line 34
4. lemma OAI.DimensionTen.Border.H_mulVec_injective line 41
5. lemma OAI.DimensionTen.Border.low_at_infinity line 49
6. lemma OAI.DimensionTen.Border.high_zero line 54
7. lemma OAI.DimensionTen.Border.no_infinity line 67
8. lemma OAI.DimensionTen.Border.minor_zero_of_rank_lt line 78
9. lemma OAI.DimensionTen.Border.homogeneousLow_chart line 87