OAI/Algebra/Determinantal/Nilpotents.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PermanentBorder.NilpotentOrbits.decomposition_of_generators line 29
  2. abbrev OAI.PermanentBorder.NilpotentOrbits.Block line 94
  3. theorem OAI.PermanentBorder.NilpotentOrbits.torsion_of_nilpotent line 96
  4. theorem OAI.PermanentBorder.NilpotentOrbits.nilpotent_decomposition line 105
  5. theorem OAI.PermanentBorder.NilpotentOrbits.nilpotent_pow_dim line 114
  6. theorem OAI.PermanentBorder.NilpotentOrbits.exponents_le_dim line 122
  7. theorem OAI.PermanentBorder.NilpotentOrbits.bounded_nilpotent_decomposition line 146
  8. theorem OAI.PermanentBorder.NilpotentOrbits.intertwiner_of_module_equiv line 154
  9. theorem OAI.PermanentBorder.NilpotentOrbits.finite_nilpotent_similarity_types line 163
  10. theorem OAI.PermanentBorder.NilpotentOrbits.unit_conjugacy_of_intertwiner line 186
  11. theorem OAI.PermanentBorder.NilpotentOrbits.finite_nilpotent_matrix_orbits line 202
  12. abbrev OAI.PermanentBorder.NilpotentBlocks.Block line 231
  13. def OAI.PermanentBorder.NilpotentBlocks.blockBasis line 233
  14. theorem OAI.PermanentBorder.NilpotentBlocks.blockBasis_apply line 236
  15. theorem OAI.PermanentBorder.NilpotentBlocks.X_smul_blockBasis line 244
  16. def OAI.PermanentBorder.NilpotentBlocks.sumBasis line 257
  17. theorem OAI.PermanentBorder.NilpotentBlocks.sumBasis_apply line 261
  18. def OAI.PermanentBorder.NilpotentBlocks.action line 269
  19. theorem OAI.PermanentBorder.NilpotentBlocks.action_sumBasis line 275
  20. def OAI.PermanentBorder.NilpotentBlocks.shiftMatrix line 292
  21. theorem OAI.PermanentBorder.NilpotentBlocks.shiftMatrix_map line 296
  22. theorem OAI.PermanentBorder.NilpotentBlocks.toMatrix_action line 302
  23. theorem OAI.PermanentBorder.NilpotentBlocks.toMatrix_of_intertwiner line 328
  24. theorem OAI.PermanentBorder.NilpotentBlocks.shift_basis_of_equiv line 339
  25. theorem OAI.PermanentBorder.NilpotentBlocks.exists_shift_basis line 351
  26. def OAI.PermanentBorder.NilpotentBlocks.indexEquiv line 375
  27. def OAI.PermanentBorder.NilpotentBlocks.shapeMatrix line 379
  28. theorem OAI.PermanentBorder.NilpotentBlocks.shapeMatrix_map line 383
  29. theorem OAI.PermanentBorder.NilpotentBlocks.exists_shape_basis line 389
  30. theorem OAI.PermanentBorder.NilpotentBlocks.matrix_conjugacy_of_basis line 401
  31. theorem OAI.PermanentBorder.NilpotentBlocks.canonical_nilpotent_form line 420