OAI/GroupTheory/FiniteType/CompressedSplittings.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CompressedSplittings.Idempotent line 13
  2. lemma OAI.CompressedSplittings.Idempotent.ext line 19
  3. def OAI.CompressedSplittings.Idempotent.coefficient line 24
  4. def OAI.CompressedSplittings.Idempotent.units line 33
  5. lemma OAI.CompressedSplittings.Idempotent.units_val line 35
  6. lemma OAI.CompressedSplittings.Idempotent.units_mul line 38
  7. lemma OAI.CompressedSplittings.Idempotent.units_conjugate line 48
  8. def OAI.CompressedSplittings.full line 60
  9. lemma OAI.CompressedSplittings.full_units line 65
  10. theorem OAI.CompressedSplittings.swindle line 70
  11. lemma OAI.CompressedSplittings.BinaryData.ds_same line 102
  12. lemma OAI.CompressedSplittings.BinaryData.ds_cross line 103
  13. def OAI.CompressedSplittings.BinaryData.projection line 105
  14. lemma OAI.CompressedSplittings.BinaryData.dd_ss line 110
  15. def OAI.CompressedSplittings.BinaryData.doubleProjection line 113
  16. lemma OAI.CompressedSplittings.BinaryData.split line 121
  17. lemma OAI.CompressedSplittings.BinaryData.subsplit line 123
  18. lemma OAI.CompressedSplittings.BinaryData.cross line 129
  19. lemma OAI.CompressedSplittings.BinaryData.subcross line 133
  20. def OAI.CompressedSplittings.BinaryData.firstExchange line 141
  21. def OAI.CompressedSplittings.BinaryData.secondExchange line 146
  22. lemma OAI.CompressedSplittings.BinaryData.firstExchange_commutes line 152
  23. lemma OAI.CompressedSplittings.BinaryData.secondExchange_commutes line 159
  24. theorem OAI.CompressedSplittings.BinaryData.annihilates line 168
  25. lemma OAI.CompressedSplittings.Idempotent.coefficient_left line 184
  26. lemma OAI.CompressedSplittings.Idempotent.coefficient_right line 189
  27. lemma OAI.CompressedSplittings.Idempotent.coefficient_orthogonal line 194
  28. lemma OAI.CompressedSplittings.Idempotent.coefficient_conjugate line 199
  29. lemma OAI.CompressedSplittings.Idempotent.steinberg_split line 206