OAI/Algebra/Determinantal/Centralizers.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PermanentBorder.Selector.fixedAffinePencil_eq_pencil line 9
  2. theorem OAI.PermanentBorder.Selector.gradient_forces_normalization_defect line 19
  3. def OAI.PermanentBorder.CentralizerDimension.centralizer line 48
  4. theorem OAI.PermanentBorder.CentralizerDimension.mem_centralizer line 60
  5. def OAI.PermanentBorder.CentralizerDimension.centralizerOne line 63
  6. def OAI.PermanentBorder.CentralizerDimension.centralizerBasis line 66
  7. def OAI.PermanentBorder.CentralizerDimension.coordinateMatrix line 70
  8. def OAI.PermanentBorder.CentralizerDimension.determinantPolynomial line 74
  9. def OAI.PermanentBorder.CentralizerDimension.singularIdeal line 78
  10. theorem OAI.PermanentBorder.CentralizerDimension.eval_coordinateMatrix line 82
  11. theorem OAI.PermanentBorder.CentralizerDimension.eval_determinantPolynomial line 92
  12. theorem OAI.PermanentBorder.CentralizerDimension.determinantPolynomial_ne_zero line 99
  13. theorem OAI.PermanentBorder.CentralizerDimension.singular_centralizer_dimension line 105
  14. theorem OAI.PermanentBorder.CentralizerDimension.nilpotent_centralizer_vanish line 116
  15. def OAI.PermanentBorder.CentralizerDimension.nilpotencyEquation line 125
  16. def OAI.PermanentBorder.CentralizerDimension.nilpotentIdeal line 129
  17. theorem OAI.PermanentBorder.CentralizerDimension.eval_nilpotencyEquation line 133
  18. theorem OAI.PermanentBorder.CentralizerDimension.nilpotentIdeal_vanishing_iff line 141
  19. theorem OAI.PermanentBorder.CentralizerDimension.singularIdeal_le_nilpotentIdeal line 165
  20. theorem OAI.PermanentBorder.CentralizerDimension.nilpotent_centralizer_dimension line 177
  21. theorem OAI.PermanentBorder.MatrixFieldExtension.rank_map line 194
  22. theorem OAI.PermanentBorder.MatrixFieldExtension.finrank_ker_map line 223
  23. def OAI.PermanentBorder.MatrixFieldExtension.mapKernel line 236
  24. theorem OAI.PermanentBorder.MatrixFieldExtension.mapKernel_linearIndependent line 246
  25. def OAI.PermanentBorder.MatrixFieldExtension.kernelBasisMap line 255
  26. theorem OAI.PermanentBorder.MatrixFieldExtension.kernelBasisMap_apply line 262
  27. def OAI.PermanentBorder.CentralizerBaseChange.equationMatrix line 274
  28. theorem OAI.PermanentBorder.CentralizerBaseChange.equationMatrix_mulVec line 278
  29. theorem OAI.PermanentBorder.CentralizerBaseChange.equationMatrix_map line 291
  30. def OAI.PermanentBorder.CentralizerBaseChange.centralizerKernelEquiv line 296
  31. theorem OAI.PermanentBorder.CentralizerBaseChange.finrank_centralizer_map line 314
  32. def OAI.PermanentBorder.CentralizerBaseChange.flatten line 326
  33. def OAI.PermanentBorder.CentralizerBaseChange.mapCentralizer line 335
  34. theorem OAI.PermanentBorder.CentralizerBaseChange.mapCentralizer_linearIndependent line 341
  35. def OAI.PermanentBorder.CentralizerBaseChange.centralizerBasisMap line 351
  36. theorem OAI.PermanentBorder.CentralizerBaseChange.centralizerBasisMap_apply line 358
  37. theorem OAI.PermanentBorder.CoordinateGauge.exists_coordinate_gauge line 369