OAI/Algebra/Determinantal/GenericPolars.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.Polar.polarValue line 11
  2. def OAI.PermanentBorder.Polar.polarGradient line 14
  3. lemma OAI.PermanentBorder.Polar.derivation_polarValue line 19
  4. lemma OAI.PermanentBorder.Polar.polar_rows_independent_of_derivations line 33
  5. lemma OAI.PermanentBorder.Polar.rows_independent_of_derivations line 79
  6. abbrev OAI.PermanentBorder.Polar.PolarVars line 156
  7. def OAI.PermanentBorder.Polar.squareJacobian line 158
  8. lemma OAI.PermanentBorder.Polar.square_isUnit_of_independent line 165
  9. lemma OAI.PermanentBorder.Polar.euler_aeval line 186
  10. lemma OAI.PermanentBorder.Polar.polar_euler_aeval line 193
  11. lemma OAI.PermanentBorder.Polar.square_mulVec_zero line 206
  12. def OAI.PermanentBorder.Polar.genericDirections line 224
  13. def OAI.PermanentBorder.Polar.genericLinear line 226
  14. lemma OAI.PermanentBorder.Polar.generic_no_infinity line 229
  15. lemma OAI.PermanentBorder.Polar.generic_square_isUnit line 247
  16. def OAI.PermanentBorder.Polar.polarPolynomial line 285
  17. def OAI.PermanentBorder.Polar.linearPolynomial line 288
  18. lemma OAI.PermanentBorder.Polar.polarPolynomial_homogeneous line 292
  19. lemma OAI.PermanentBorder.Polar.linearPolynomial_homogeneous line 299
  20. lemma OAI.PermanentBorder.Polar.det_row_homogeneous line 305
  21. def OAI.PermanentBorder.Polar.squarePolynomial line 319
  22. def OAI.PermanentBorder.Polar.squareDegrees line 327
  23. lemma OAI.PermanentBorder.Polar.squarePolynomial_homogeneous line 332
  24. def OAI.PermanentBorder.Polar.badPolarSystem line 343
  25. def OAI.PermanentBorder.Polar.badPolarDegrees line 351
  26. lemma OAI.PermanentBorder.Polar.badPolarSystem_homogeneous line 357
  27. lemma OAI.PermanentBorder.Polar.eval_polarPolynomial line 372
  28. lemma OAI.PermanentBorder.Polar.eval_linearPolynomial line 377
  29. lemma OAI.PermanentBorder.Polar.eval_squarePolynomial line 381
  30. lemma OAI.PermanentBorder.Polar.map_polarPolynomial line 401
  31. lemma OAI.PermanentBorder.Polar.map_linearPolynomial line 405
  32. lemma OAI.PermanentBorder.Polar.map_squarePolynomial line 409
  33. lemma OAI.PermanentBorder.Polar.map_badPolarSystem line 420