OAI/Analysis/Quantum/DimensionTen/AlphaMinors.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DimensionTen.Border.C_relation line 11
2. lemma OAI.DimensionTen.Border.map_int_rat line 19
3. lemma OAI.DimensionTen.Border.high_alpha line 25
4. lemma OAI.DimensionTen.Border.minors_alpha line 31
5. lemma OAI.DimensionTen.Border.mon_map line 45
6. lemma OAI.DimensionTen.Border.low_map line 49
7. lemma OAI.DimensionTen.Border.pencilR_map line 53
8. lemma OAI.DimensionTen.Border.minor_map line 58
9. lemma OAI.DimensionTen.Border.minors_embedding line 63