OAI/Algebra/Determinantal/BilinearCounts.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.PolarAnalysis.finite_simple_polar_kernel_lifts line 11
  2. abbrev OAI.PermanentBorder.KernelBilinear.ChartSpace line 66
  3. def OAI.PermanentBorder.KernelBilinear.optionProduct line 67
  4. lemma OAI.PermanentBorder.KernelBilinear.optionProduct_apply line 69
  5. lemma OAI.PermanentBorder.KernelBilinear.optionProduct_symm_apply line 70
  6. lemma OAI.PermanentBorder.KernelBilinear.pivot_symm line 73
  7. lemma OAI.PermanentBorder.KernelBilinear.pivot_symm_succAbove line 75
  8. def OAI.PermanentBorder.KernelBilinear.norm line 79
  9. lemma OAI.PermanentBorder.KernelBilinear.norm_pivot line 81
  10. lemma OAI.PermanentBorder.KernelBilinear.norm_succAbove line 84
  11. def OAI.PermanentBorder.KernelBilinear.chart line 89
  12. def OAI.PermanentBorder.KernelBilinear.base line 91
  13. lemma OAI.PermanentBorder.KernelBilinear.base_group line 96
  14. lemma OAI.PermanentBorder.KernelBilinear.chart_base line 98
  15. lemma OAI.PermanentBorder.KernelBilinear.contDiff_chart line 101
  16. def OAI.PermanentBorder.KernelBilinear.outputLinear line 111
  17. def OAI.PermanentBorder.KernelBilinear.output line 139
  18. lemma OAI.PermanentBorder.KernelBilinear.chart_separated line 142
  19. lemma OAI.PermanentBorder.KernelBilinear.sum_norm line 156
  20. lemma OAI.PermanentBorder.KernelBilinear.polar_norm line 161
  21. lemma OAI.PermanentBorder.KernelBilinear.system_eq_matrixKernelSystem line 176
  22. theorem OAI.PermanentBorder.KernelBilinear.selected_kernel_count line 261
  23. def OAI.PermanentBorder.KernelBilinear.affine line 304
  24. lemma OAI.PermanentBorder.KernelBilinear.affine_contDiff line 308
  25. lemma OAI.PermanentBorder.KernelBilinear.affine_derivative line 315
  26. lemma OAI.PermanentBorder.KernelBilinear.affine_right_mul line 327
  27. theorem OAI.PermanentBorder.KernelBilinear.affine_polar_count line 333