OAI/GroupTheory/FiniteType/RingExchange.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.RingExchange.Data line 12
  2. lemma OAI.RingExchange.Data.Ea line 28
  3. lemma OAI.RingExchange.Data.aF line 29
  4. lemma OAI.RingExchange.Data.Fb line 30
  5. lemma OAI.RingExchange.Data.bE line 31
  6. lemma OAI.RingExchange.Data.aa line 32
  7. lemma OAI.RingExchange.Data.bb line 35
  8. lemma OAI.RingExchange.Data.EE line 38
  9. lemma OAI.RingExchange.Data.FF line 41
  10. def OAI.RingExchange.Data.value line 45
  11. lemma OAI.RingExchange.Data.square line 47
  12. lemma OAI.RingExchange.Data.value_E line 52
  13. lemma OAI.RingExchange.Data.a_value line 55
  14. def OAI.RingExchange.Data.unit line 59
  15. lemma OAI.RingExchange.Data.conjugates line 61
  16. lemma OAI.RingExchange.Data.commutes line 65
  17. def OAI.RingExchange.ofPairs line 70
  18. def OAI.Steinberg.blockUpper line 91
  19. def OAI.Steinberg.blockLower line 97
  20. lemma OAI.Steinberg.matrix_blockUpper line 103
  21. lemma OAI.Steinberg.matrix_blockLower line 126
  22. def OAI.Steinberg.blockBalanced line 149
  23. lemma OAI.Steinberg.matrix_blockBalanced line 153
  24. def OAI.RingExchange.Data.flipMatrix line 163
  25. lemma OAI.RingExchange.Data.flipMatrix_square line 165
  26. def OAI.RingExchange.Data.flipUnit line 174
  27. lemma OAI.RingExchange.Data.flip_bad_row line 177
  28. lemma OAI.RingExchange.Data.flip_bad_col line 182
  29. abbrev OAI.Steinberg.SixIndices line 193
  30. def OAI.Steinberg.retainedIndices line 195
  31. lemma OAI.Steinberg.flip_kernel_central line 200
  32. def OAI.Steinberg.diagonalAction line 261
  33. lemma OAI.Steinberg.diagonalAction_root line 271
  34. lemma OAI.Steinberg.diagonalAction_mul line 274
  35. lemma OAI.Steinberg.diagonalAction_one line 280
  36. lemma OAI.Steinberg.conjugate_diagonal_column line 287
  37. lemma OAI.Steinberg.conjugate_diagonal_row line 305
  38. lemma OAI.Steinberg.conjugate_block_diagonal line 323
  39. def OAI.Steinberg.transportWord line 364
  40. lemma OAI.Steinberg.matrix_transportWord line 368
  41. lemma OAI.Steinberg.matrix_transportWord_inv line 377
  42. lemma OAI.Steinberg.constantPair_inner line 391
  43. lemma OAI.Steinberg.innerWeights_mul line 406
  44. def OAI.Steinberg.scalarWeight₀ line 417
  45. def OAI.Steinberg.scalarWeight₁ line 421
  46. def OAI.Steinberg.scalarWeight₂ line 425
  47. lemma OAI.Steinberg.scalarWeight_product line 429
  48. lemma OAI.Steinberg.scalar_involution_inner line 434
  49. lemma OAI.Steinberg.central_conjugated_coefficients line 469