OAI/Algebra/Determinantal/SchurLifts.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PermanentBorder.PolarAnalysis.Schur.dirMatrix line 11
  2. def OAI.PermanentBorder.PolarAnalysis.Schur.kernelRemaining line 15
  3. theorem OAI.PermanentBorder.PolarAnalysis.Schur.kernelRemaining_solved line 25
  4. theorem OAI.PermanentBorder.PolarAnalysis.Schur.contDiff_block line 43
  5. theorem OAI.PermanentBorder.PolarAnalysis.Schur.differentiableAt_kernelRemaining line 58
  6. theorem OAI.PermanentBorder.PolarAnalysis.Schur.simple_kernel_lift line 99
  7. def OAI.PermanentBorder.PolarAnalysis.Schur.affineValue line 155
  8. theorem OAI.PermanentBorder.PolarAnalysis.Schur.affineValue_contDiff line 162
  9. theorem OAI.PermanentBorder.PolarAnalysis.Schur.block_entries line 171
  10. theorem OAI.PermanentBorder.PolarAnalysis.Schur.simple_affine_kernel_lift line 177
  11. def OAI.PermanentBorder.PolarAnalysis.dotLinear line 210
  12. theorem OAI.PermanentBorder.PolarAnalysis.exists_common_functional line 215
  13. theorem OAI.PermanentBorder.PolarAnalysis.det_updateRow_one line 229
  14. theorem OAI.PermanentBorder.PolarAnalysis.exists_common_kernel_chart line 237
  15. def OAI.PermanentBorder.PolarAnalysis.determinantMultilinear line 285
  16. theorem OAI.PermanentBorder.PolarAnalysis.determinantDifferential line 290
  17. theorem OAI.PermanentBorder.PolarAnalysis.differentiableAt_determinant line 305
  18. theorem OAI.PermanentBorder.PolarAnalysis.adjugate_ne_zero_of_differential line 309
  19. theorem OAI.PermanentBorder.PolarAnalysis.first_derivative_ne_zero_of_invertible line 332
  20. theorem OAI.PermanentBorder.PolarAnalysis.selected_simple_common_kernel_chart line 346
  21. def OAI.PermanentBorder.PolarAnalysis.unitSumOptionEquiv line 366
  22. def OAI.PermanentBorder.PolarAnalysis.pivotEquiv line 375
  23. theorem OAI.PermanentBorder.PolarAnalysis.pivotEquiv_inl line 378
  24. theorem OAI.PermanentBorder.PolarAnalysis.pivotEquiv_inr line 380
  25. theorem OAI.PermanentBorder.PolarAnalysis.det_submatrix_two_equiv line 383
  26. theorem OAI.PermanentBorder.PolarAnalysis.determinant_pivot_scalar line 389
  27. theorem OAI.PermanentBorder.PolarAnalysis.pivot_minor_ne_zero line 396
  28. def OAI.PermanentBorder.PolarAnalysis.Schur.matrixKernelSystem line 412
  29. def OAI.PermanentBorder.PolarAnalysis.Schur.matrixKernelPoint line 423
  30. theorem OAI.PermanentBorder.PolarAnalysis.Schur.simple_matrix_kernel_lift line 430