OAI/GroupTheory/FiniteType/SteinbergSixThree.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Steinberg.six_three line 13
  2. lemma OAI.Steinberg.exchange_coefficient_kernel_central line 30
  3. lemma OAI.Steinberg.exchange_coefficient_kernel_equal line 37
  4. theorem OAI.Steinberg.binary_kernel_annihilation_six line 47
  5. lemma OAI.Steinberg.map_reindex line 81
  6. lemma OAI.Steinberg.reindex_equiv_symm line 89
  7. def OAI.Steinberg.sixEquiv line 97
  8. theorem OAI.Steinberg.binary_kernel_annihilation line 100
  9. theorem OAI.Steinberg.kernelAnnihilationObligation line 112
  10. lemma OAI.NoncommElementary.positions_commute line 121
  11. lemma OAI.NoncommElementary.position_normalizes line 133
  12. lemma OAI.NoncommElementary.position_commutator_mem line 137
  13. def OAI.NoncommElementary.diagonalKernel line 154
  14. instance OAI.NoncommElementary.diagonalKernel_normal line 156
  15. lemma OAI.NoncommElementary.quotient_commute line 162
  16. lemma OAI.NoncommElementary.quotient_conjugate line 170
  17. theorem OAI.NoncommElementary.compressed_diagonal line 180
  18. def OAI.NoncommElementary.compressed line 188
  19. lemma OAI.NoncommElementary.compressed_coe line 194
  20. def OAI.Steinberg.descended line 203
  21. lemma OAI.Steinberg.descended_pi line 208
  22. lemma OAI.Steinberg.matrix_descended line 212
  23. def OAI.Steinberg.unitLift line 218
  24. lemma OAI.Steinberg.matrixCoefficient_position line 222
  25. lemma OAI.Steinberg.units_comp line 232
  26. theorem OAI.Steinberg.matrix_unitLift line 239