OAI/Algebra/Determinantal/RegularSections.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.CI.linear line 11
  2. def OAI.PermanentBorder.CI.normalized line 14
  3. def OAI.PermanentBorder.CI.square line 17
  4. def OAI.PermanentBorder.CI.bad line 21
  5. def OAI.PermanentBorder.CI.degrees line 24
  6. lemma OAI.PermanentBorder.CI.linear_homogeneous line 26
  7. lemma OAI.PermanentBorder.CI.pderiv_linear line 31
  8. lemma OAI.PermanentBorder.CI.pderiv_normalized line 35
  9. lemma OAI.PermanentBorder.CI.eval_linear line 39
  10. lemma OAI.PermanentBorder.CI.det_homogeneous line 42
  11. lemma OAI.PermanentBorder.CI.square_det_homogeneous line 56
  12. lemma OAI.PermanentBorder.CI.bad_homogeneous line 67
  13. def OAI.PermanentBorder.CI.Good line 78
  14. lemma OAI.PermanentBorder.CI.good_iff_bad line 82
  15. def OAI.PermanentBorder.CI.powers line 108
  16. def OAI.PermanentBorder.CI.coordinate line 110
  17. lemma OAI.PermanentBorder.CI.powers_homogeneous line 113
  18. lemma OAI.PermanentBorder.CI.eval_coordinate line 117
  19. lemma OAI.PermanentBorder.CI.powers_good line 120
  20. def OAI.PermanentBorder.CI.Roots line 171
  21. def OAI.PermanentBorder.CI.powersRootsEquiv line 174
  22. lemma OAI.PermanentBorder.CI.card_power_roots line 194
  23. lemma OAI.PermanentBorder.CI.powers_card line 201
  24. def OAI.PermanentBorder.CI.polynomialDerivative line 213
  25. lemma OAI.PermanentBorder.CI.polynomialDerivative_apply line 217
  26. lemma OAI.PermanentBorder.CI.hasFDerivAt_eval line 222
  27. lemma OAI.PermanentBorder.CI.contDiff_eval line 251
  28. def OAI.PermanentBorder.CI.jacobian line 258
  29. lemma OAI.PermanentBorder.CI.system_fderiv line 261
  30. lemma OAI.PermanentBorder.CI.system_fderiv_apply line 266
  31. lemma OAI.PermanentBorder.CI.system_fderiv_invertible line 272
  32. theorem OAI.PermanentBorder.Polar.localHomeomorph_restrictPreimage line 291
  33. theorem OAI.PermanentBorder.Polar.zero_projection_chart line 308
  34. theorem OAI.PermanentBorder.Polar.implicit_zero_projection line 337
  35. theorem OAI.PermanentBorder.Polar.covering_card_locallyConstant line 351
  36. theorem OAI.PermanentBorder.Polar.proper_localHomeomorph_card line 361
  37. theorem OAI.PermanentBorder.Polar.localHomeomorphOn_restrictPreimage line 382
  38. theorem OAI.PermanentBorder.Polar.implicit_zero_projection_on line 400
  39. theorem OAI.PermanentBorder.Polar.homogeneous_normalized_proper line 421