OAI/Analysis/GroupDeterminants/Lamps.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LampDraft.FullLamp line 13
  2. def OAI.LampDraft.coordinate line 15
  3. def OAI.LampDraft.lampSubgroup line 19
  4. abbrev OAI.LampDraft.LampGroup line 23
  5. instance OAI.LampDraft.lampGroup_fg line 25
  6. def OAI.LampDraft.shift line 31
  7. def OAI.LampDraft.lampSeed line 36
  8. def OAI.LampDraft.lamp line 40
  9. theorem OAI.LampDraft.shift_coe line 42
  10. theorem OAI.LampDraft.lamp_coe line 44
  11. theorem OAI.LampDraft.lamp_commute line 55
  12. theorem OAI.LampDraft.lamp_cube line 60
  13. theorem OAI.LampDraft.shift_conjugate_lamp line 73
  14. theorem OAI.LampDraft.shift_injective line 78
  15. def OAI.LampDraft.lampRight line 82
  16. abbrev OAI.LampDraft.BaseGroup line 85
  17. instance OAI.LampDraft.baseGroup_commGroup line 87
  18. def OAI.LampDraft.baseLamp line 104
  19. def OAI.LampDraft.baseCoordinate line 108
  20. lemma OAI.LampDraft.baseCoordinate_baseLamp line 117
  21. lemma OAI.LampDraft.baseCoordinate_injective line 123
  22. lemma OAI.LampDraft.baseLamp_cube line 131
  23. lemma OAI.LampDraft.baseLamp_ne_one line 135
  24. lemma OAI.LampDraft.baseLamp_sq_ne_one line 140