OAI/Geometry/HarmonicGrowth/AngularTrace.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HarmonicCounterexample.Angular.planeMatrix line 13
  2. lemma OAI.HarmonicCounterexample.Angular.planeMatrix_skew line 16
  3. lemma OAI.HarmonicCounterexample.Angular.planeField_apply line 20
  4. lemma OAI.HarmonicCounterexample.Angular.linearField_plane_X line 24
  5. def OAI.HarmonicCounterexample.Angular.plane line 29
  6. lemma OAI.HarmonicCounterexample.Angular.plane_val line 37
  7. lemma OAI.HarmonicCounterexample.Angular.plane_self line 40
  8. lemma OAI.HarmonicCounterexample.Angular.plane_swap line 43
  9. lemma OAI.HarmonicCounterexample.Angular.planeMatrix_eq_single line 46
  10. lemma OAI.HarmonicCounterexample.Angular.single_product line 52
  11. lemma OAI.HarmonicCounterexample.Angular.indicator_sub line 59
  12. lemma OAI.HarmonicCounterexample.Angular.map_indicator line 63
  13. lemma OAI.HarmonicCounterexample.Angular.planeMatrix_commutator line 68
  14. lemma OAI.HarmonicCounterexample.Angular.plane_field_val line 77
  15. lemma OAI.HarmonicCounterexample.Angular.linearFieldMap_apply line 81
  16. lemma OAI.HarmonicCounterexample.Angular.plane_bracket line 84
  17. lemma OAI.HarmonicCounterexample.Angular.end_sub_zero line 115
  18. lemma OAI.HarmonicCounterexample.Angular.end_zero_sub line 116
  19. lemma OAI.HarmonicCounterexample.Angular.end_zero_add line 117
  20. lemma OAI.HarmonicCounterexample.Angular.end_add_zero line 118
  21. lemma OAI.HarmonicCounterexample.Angular.end_neg_neg line 119
  22. lemma OAI.HarmonicCounterexample.Angular.end_neg_mul line 120
  23. lemma OAI.HarmonicCounterexample.Angular.end_mul_neg line 121
  24. lemma OAI.HarmonicCounterexample.Angular.end_mul_zero line 122
  25. lemma OAI.HarmonicCounterexample.Angular.end_trace_neg line 123
  26. lemma OAI.HarmonicCounterexample.Angular.end_trace_add line 124
  27. lemma OAI.HarmonicCounterexample.Angular.end_trace_sub line 126
  28. lemma OAI.HarmonicCounterexample.Angular.end_trace_smul line 128
  29. lemma OAI.HarmonicCounterexample.Angular.end_trace_sum line 130
  30. lemma OAI.HarmonicCounterexample.Angular.plane_triple line 134
  31. lemma OAI.HarmonicCounterexample.Angular.plane_triple' line 141
  32. lemma OAI.HarmonicCounterexample.Angular.plane_disjoint line 147
  33. lemma OAI.HarmonicCounterexample.Angular.trace_comm_self line 151
  34. def OAI.HarmonicCounterexample.Angular.planePair line 156
  35. lemma OAI.HarmonicCounterexample.Angular.pair_comm line 159
  36. lemma OAI.HarmonicCounterexample.Angular.pair_self line 162
  37. lemma OAI.HarmonicCounterexample.Angular.pair_swap_left line 165
  38. lemma OAI.HarmonicCounterexample.Angular.pair_swap_right line 169
  39. lemma OAI.HarmonicCounterexample.Angular.pair_shared line 173
  40. lemma OAI.HarmonicCounterexample.Angular.pair_square_shared line 180
  41. lemma OAI.HarmonicCounterexample.Angular.fifth_index line 203
  42. lemma OAI.HarmonicCounterexample.Angular.pair_square_swap line 221
  43. lemma OAI.HarmonicCounterexample.Angular.pair_square_common line 224
  44. lemma OAI.HarmonicCounterexample.Angular.pair_square_all line 230
  45. lemma OAI.HarmonicCounterexample.Angular.pair_disjoint_zero line 240
  46. lemma OAI.HarmonicCounterexample.Angular.pair_formula line 249
  47. lemma OAI.HarmonicCounterexample.Angular.polynomial_plane_square line 291
  48. lemma OAI.HarmonicCounterexample.Angular.euler_second line 302
  49. lemma OAI.HarmonicCounterexample.Angular.sum_plane_square line 322
  50. lemma OAI.HarmonicCounterexample.Angular.casimir line 355
  51. lemma OAI.HarmonicCounterexample.Angular.trace_smul_square line 376
  52. lemma OAI.HarmonicCounterexample.Angular.trace_square_sum line 381
  53. lemma OAI.HarmonicCounterexample.Angular.rotation_sum_planes line 392
  54. lemma OAI.HarmonicCounterexample.Angular.plane_square_trace16 line 409
  55. lemma OAI.HarmonicCounterexample.Angular.rotation_trace16 line 436
  56. lemma OAI.HarmonicCounterexample.Angular.rotation_square_trace16 line 474