OAI/Geometry/Arnold/Kernel.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArnoldCounterexample.Construction.kernelVector line 16
  2. lemma OAI.ArnoldCounterexample.Construction.kernelVector_ne_zero line 18
  3. lemma OAI.ArnoldCounterexample.Construction.kernelVector_horizontal line 23
  4. lemma OAI.ArnoldCounterexample.Construction.zero_left line 28
  5. lemma OAI.ArnoldCounterexample.Construction.zero_right line 29
  6. lemma OAI.ArnoldCounterexample.Construction.zero_casimir line 30
  7. lemma OAI.ArnoldCounterexample.Construction.zero_pairing line 31
  8. lemma OAI.ArnoldCounterexample.Construction.zero_leftOperator line 35
  9. lemma OAI.ArnoldCounterexample.Construction.zero_rightOperator line 43
  10. lemma OAI.ArnoldCounterexample.Construction.left_kernel line 51
  11. lemma OAI.ArnoldCounterexample.Construction.right_kernel line 56
  12. lemma OAI.ArnoldCounterexample.Construction.zero_operator_cancel line 61
  13. def OAI.ArnoldCounterexample.Construction.kernelCurve line 66
  14. lemma OAI.ArnoldCounterexample.Construction.kernelCurve_zero line 67
  15. lemma OAI.ArnoldCounterexample.Construction.kernelCurve_derivative line 68
  16. lemma OAI.ArnoldCounterexample.Construction.left_curve line 72
  17. lemma OAI.ArnoldCounterexample.Construction.right_curve line 75
  18. lemma OAI.ArnoldCounterexample.Construction.casimir_curve line 79
  19. lemma OAI.ArnoldCounterexample.Construction.pairing_curve line 84
  20. lemma OAI.ArnoldCounterexample.Construction.mixed_curve line 89
  21. lemma OAI.ArnoldCounterexample.Construction.core_curve line 98
  22. lemma OAI.ArnoldCounterexample.Construction.core_kernel line 122
  23. lemma OAI.ArnoldCounterexample.Construction.vectorField_zeroVector line 126
  24. lemma OAI.ArnoldCounterexample.Construction.vectorField_kernel line 129