OAI/Algebra/FormalGroup/Honda/Leading.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HeightThree.HondaLeading.pair line 11
2. lemma OAI.HeightThree.HondaLeading.pair_const line 12
3. lemma OAI.HeightThree.HondaLeading.pair_linear line 17
4. abbrev OAI.HeightThree.HondaLeading.leading line 29
5. lemma OAI.HeightThree.HondaLeading.leading_approx line 31
6. lemma OAI.HeightThree.HondaLeading.leading_homogeneous line 36
7. lemma OAI.HeightThree.HondaLeading.homogeneous_zero line 39
8. lemma OAI.HeightThree.HondaLeading.homogeneous_C_mul line 42
9. lemma OAI.HeightThree.HondaLeading.linear_pair_homogeneous line 46
10. lemma OAI.HeightThree.HondaLeading.leading_axis line 57
11. lemma OAI.HeightThree.HondaLeading.leading_symmetric line 79
12. lemma OAI.HeightThree.HondaLeading.leading_evaluate line 91
13. lemma OAI.HeightThree.HondaLeading.leading_variation line 110
14. lemma OAI.HeightThree.HondaLeading.leading_associative line 128
15. lemma OAI.HeightThree.HondaLeading.multiplication_zero line 192
16. lemma OAI.HeightThree.HondaLeading.multiplication_succ line 193
17. lemma OAI.HeightThree.HondaLeading.multiplication_constant line 198
18. lemma OAI.HeightThree.HondaLeading.multiplication_linear line 206
19. lemma OAI.HeightThree.HondaLeading.multiplication_match line 218
20. lemma OAI.HeightThree.HondaLeading.multiplication_leading_trace line 236
21. lemma OAI.HeightThree.HondaLeading.homogeneous_sum line 258
22. lemma OAI.HeightThree.HondaLeading.leading_trace_zero line 266
23. theorem OAI.HeightThree.HondaLeading.leading_isCocycle line 281