OAI/Algebra/PolynomialChains/Real.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Real weighted chains and pure-power squarefreeness.

  1. abbrev OAI.MultiplicityCounterexample.ComplexAffine line 12
  2. abbrev OAI.MultiplicityCounterexample.RealPolynomial line 13
  3. def OAI.MultiplicityCounterexample.complexEval line 15
  4. def OAI.MultiplicityCounterexample.hypersurface line 18
  5. def OAI.MultiplicityCounterexample.IsReduced line 21
  6. def OAI.MultiplicityCounterexample.orderAtOrigin line 24
  7. def OAI.MultiplicityCounterexample.IsPositivelyWeightedHomogeneous line 27
  8. def OAI.MultiplicityCounterexample.IsCriticalPoint line 33
  9. def OAI.MultiplicityCounterexample.HasIsolatedCriticalPointAtOrigin line 36
  10. def OAI.MultiplicityCounterexample.AmbientlyHomeomorphicAtOrigin line 41
  11. def OAI.MultiplicityCounterexample.Chains.polynomial line 57
  12. lemma OAI.MultiplicityCounterexample.Chains.map_polynomial line 62
  13. lemma OAI.MultiplicityCounterexample.Chains.tail_decomposition line 68
  14. def OAI.MultiplicityCounterexample.Chains.next line 79
  15. def OAI.MultiplicityCounterexample.Chains.previous line 82
  16. lemma OAI.MultiplicityCounterexample.Chains.next_castSucc line 85
  17. lemma OAI.MultiplicityCounterexample.Chains.next_last line 87
  18. lemma OAI.MultiplicityCounterexample.Chains.previous_zero line 89
  19. lemma OAI.MultiplicityCounterexample.Chains.previous_succ line 91
  20. lemma OAI.MultiplicityCounterexample.Chains.eval_pderiv line 95
  21. lemma OAI.MultiplicityCounterexample.Chains.previous_eq_zero_of_first line 134
  22. theorem OAI.MultiplicityCounterexample.Chains.critical_locus line 148
  23. lemma OAI.MultiplicityCounterexample.Chains.eval_scale line 194
  24. lemma OAI.MultiplicityCounterexample.Chains.monomial_degrees line 211
  25. theorem OAI.MultiplicityCounterexample.Chains.exists_chain_data line 226
  26. lemma OAI.MultiplicityCounterexample.complexEval_chain line 267
  27. lemma OAI.MultiplicityCounterexample.complexEval_pderiv_chain line 272
  28. theorem OAI.MultiplicityCounterexample.real_chain_critical_iff line 278
  29. theorem OAI.MultiplicityCounterexample.real_chain_isolated line 284
  30. theorem OAI.MultiplicityCounterexample.real_chain_weighted line 291
  31. theorem OAI.MultiplicityCounterexample.real_chain_order_ge_three line 301
  32. theorem OAI.MultiplicityCounterexample.exists_real_chain line 308
  33. lemma OAI.MultiplicityCounterexample.squarefree_of_pderiv_power line 347
  34. lemma OAI.MultiplicityCounterexample.squarefree_add_pure_power line 366
  35. theorem OAI.MultiplicityCounterexample.isReduced_add_pure_power line 387