OAI/Analysis/LienardCycles/AlgebraicNotation.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.(instance at line 19) line 19
  2. instance OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.(instance at line 20) line 20
  3. instance OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.(instance at line 21) line 21
  4. instance OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.(instance at line 22) line 22
  5. instance OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.(instance at line 23) line 23
  6. instance OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.(instance at line 24) line 24
  7. instance OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.(instance at line 25) line 25
  8. def OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.pow line 26
  9. instance OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.(instance at line 29) line 29
  10. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_const line 30
  11. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_linear line 31
  12. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_add line 32
  13. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_mul line 33
  14. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_inv line 34
  15. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_neg line 35
  16. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_sub line 36
  17. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_div line 37
  18. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_ofNat line 38
  19. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_pow line 39
  20. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.eval_sqrt line 46
  21. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_const line 47
  22. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_linear line 48
  23. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_add line 49
  24. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_mul line 50
  25. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_inv line 51
  26. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_neg line 52
  27. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_sub line 53
  28. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_div line 54
  29. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_ofNat line 55
  30. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_pow line 56
  31. lemma OAI.QuinticLienard.SmoothFlow.AlgebraicExpr.regular_sqrt line 60