OAI/Analysis/Quantum/PPTSquare/SplittingField.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PencilField.f line 14
2. abbrev OAI.PencilField.K line 15
3. lemma OAI.PencilField.reduction41 line 19
4. lemma OAI.PencilField.reduction131 line 21
5. lemma OAI.PencilField.reduction139 line 23
6. lemma OAI.PencilField.gcd_bridge41 line 27
7. lemma OAI.PencilField.gcd_bridge131 line 31
8. lemma OAI.PencilField.gcd_bridge139 line 35
9. lemma OAI.PencilField.reduction_gcd41 line 39
10. lemma OAI.PencilField.reduction_gcd131 line 44
11. lemma OAI.PencilField.reduction_gcd139 line 49
12. lemma OAI.PencilField.exists_field_data line 55
13. lemma OAI.PencilField.exists_complex_data line 110