OAI/GroupTheory/SimpleOvergroups/RingAssemblyTools.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleFInftyOvergroups.RingAssembly.differences line 19
  2. theorem OAI.SimpleFInftyOvergroups.RingAssembly.differences_finite line 21
  3. theorem OAI.SimpleFInftyOvergroups.RingAssembly.ker_ringQuot line 24
  4. theorem OAI.SimpleFInftyOvergroups.RingAssembly.supportIdempotent line 49
  5. def OAI.SimpleFInftyOvergroups.RingAssembly.toCorner line 53
  6. theorem OAI.SimpleFInftyOvergroups.RingAssembly.toCorner_injective line 61
  7. theorem OAI.SimpleFInftyOvergroups.RingAssembly.monoidBasis_injective line 70
  8. def OAI.SimpleFInftyOvergroups.RingAssembly.monoidBasisâ‚€ line 81
  9. def OAI.SimpleFInftyOvergroups.RingAssembly.binaryS line 88
  10. def OAI.SimpleFInftyOvergroups.RingAssembly.binaryD line 89
  11. lemma OAI.SimpleFInftyOvergroups.RingAssembly.q_binaryS line 91
  12. lemma OAI.SimpleFInftyOvergroups.RingAssembly.binaryS_q line 95
  13. lemma OAI.SimpleFInftyOvergroups.RingAssembly.q_binaryD line 99
  14. lemma OAI.SimpleFInftyOvergroups.RingAssembly.binaryD_q line 103
  15. lemma OAI.SimpleFInftyOvergroups.RingAssembly.binaryDS line 107
  16. lemma OAI.SimpleFInftyOvergroups.RingAssembly.binary_partition line 110
  17. def OAI.SimpleFInftyOvergroups.RingAssembly.binaryPhi line 115
  18. lemma OAI.SimpleFInftyOvergroups.RingAssembly.binaryPhi_apply line 117
  19. lemma OAI.SimpleFInftyOvergroups.RingAssembly.binary_constant_commute line 119
  20. def OAI.SimpleFInftyOvergroups.RingAssembly.binaryData line 126
  21. theorem OAI.SimpleFInftyOvergroups.RingAssembly.binaryPhi_injective line 153