OAI/Algebra/Determinantal/KernelCharts.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PermanentBorder.Multigraded.weight_mapDomain_eq line 9
  2. lemma OAI.PermanentBorder.Multigraded.homogeneous_rename line 17
  3. theorem OAI.PermanentBorder.Multigraded.bilinear_simple_point_count_reindex line 34
  4. abbrev OAI.PermanentBorder.KernelBilinear.Groups line 100
  5. abbrev OAI.PermanentBorder.KernelBilinear.Var line 101
  6. instance OAI.PermanentBorder.KernelBilinear.varFintype line 103
  7. abbrev OAI.PermanentBorder.KernelBilinear.Variables line 106
  8. abbrev OAI.PermanentBorder.KernelBilinear.Equations line 107
  9. def OAI.PermanentBorder.KernelBilinear.dimensions line 111
  10. lemma OAI.PermanentBorder.KernelBilinear.dimensions_none line 114
  11. lemma OAI.PermanentBorder.KernelBilinear.dimensions_some line 115
  12. lemma OAI.PermanentBorder.KernelBilinear.var_card line 117
  13. def OAI.PermanentBorder.KernelBilinear.variablesEquiv line 126
  14. lemma OAI.PermanentBorder.KernelBilinear.variablesEquiv_group line 131
  15. def OAI.PermanentBorder.KernelBilinear.linearMatrix line 134
  16. def OAI.PermanentBorder.KernelBilinear.rightEquation line 139
  17. def OAI.PermanentBorder.KernelBilinear.leftEquation line 144
  18. def OAI.PermanentBorder.KernelBilinear.polarEquation line 149
  19. def OAI.PermanentBorder.KernelBilinear.system line 153
  20. def OAI.PermanentBorder.KernelBilinear.firstGroup line 160
  21. def OAI.PermanentBorder.KernelBilinear.secondGroup line 162
  22. lemma OAI.PermanentBorder.KernelBilinear.linearMatrix_homogeneous line 165
  23. lemma OAI.PermanentBorder.KernelBilinear.right_homogeneous line 173
  24. lemma OAI.PermanentBorder.KernelBilinear.left_homogeneous line 183
  25. lemma OAI.PermanentBorder.KernelBilinear.polar_homogeneous line 194
  26. lemma OAI.PermanentBorder.KernelBilinear.system_homogeneous line 205
  27. lemma OAI.PermanentBorder.KernelBilinear.card_equations line 216
  28. def OAI.PermanentBorder.KernelBilinear.coordinates line 220
  29. lemma OAI.PermanentBorder.KernelBilinear.eval_linearMatrix line 227
  30. lemma OAI.PermanentBorder.KernelBilinear.eval_right line 233
  31. lemma OAI.PermanentBorder.KernelBilinear.eval_left line 240
  32. lemma OAI.PermanentBorder.KernelBilinear.eval_polar line 248
  33. lemma OAI.PermanentBorder.KernelBilinear.mixedPolynomial_eq line 253
  34. def OAI.PermanentBorder.Multigraded.collapse line 266
  35. lemma OAI.PermanentBorder.Multigraded.collapse_monomial line 269
  36. lemma OAI.PermanentBorder.Multigraded.coeff_le_collapse line 279
  37. lemma OAI.PermanentBorder.KernelBilinear.mixed_coefficient_bound line 298
  38. theorem OAI.PermanentBorder.PolarAnalysis.isInvertible_of_injective line 326
  39. theorem OAI.PermanentBorder.PolarAnalysis.invertible_elimination line 332
  40. theorem OAI.PermanentBorder.PolarAnalysis.simple_after_elimination line 363
  41. def OAI.PermanentBorder.PolarAnalysis.Schur.block line 392
  42. def OAI.PermanentBorder.PolarAnalysis.Schur.right line 395
  43. def OAI.PermanentBorder.PolarAnalysis.Schur.left line 396
  44. def OAI.PermanentBorder.PolarAnalysis.Schur.scalar line 397
  45. def OAI.PermanentBorder.PolarAnalysis.Schur.normalized line 399
  46. theorem OAI.PermanentBorder.PolarAnalysis.Schur.solved_right line 401
  47. theorem OAI.PermanentBorder.PolarAnalysis.Schur.solved_left line 412
  48. theorem OAI.PermanentBorder.PolarAnalysis.Schur.det_block line 429
  49. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differentiableAt_det line 443
  50. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differentiableAt_adjugate line 450
  51. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differentiableAt_inverse line 462