OAI/GroupTheory/ArtinCAT0/Mirrors.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ArtinCAT0.Mirror line 7
  2. def OAI.ArtinCAT0.sideMirror line 9
  3. def OAI.ArtinCAT0.extraMirror line 12
  4. def OAI.ArtinCAT0.mirrorReflect line 17

    Source documentation

    Action on x=k, y=k, x+y=k for the three side reflections of the triangle x≥0, y≥0, x+y≤1 in equilateral coordinates.

    def mirrorReflect (u : Fin 3) (d : Mirror) : Mirror :=
…

    Mentions: OAI.ArtinCAT0.Mirror

  5. lemma OAI.ArtinCAT0.mirrorReflect_involutive line 25
  6. lemma OAI.ArtinCAT0.mirrorReflect_braid line 29
  7. def OAI.ArtinCAT0.mirrorPerm line 35
  8. lemma OAI.ArtinCAT0.mirrorPerm_apply line 37
  9. lemma OAI.ArtinCAT0.mirrorPerm_symm_apply line 38
  10. lemma OAI.ArtinCAT0.mirrorPerm_braid line 41
  11. lemma OAI.ArtinCAT0.mirrorReflect_side line 48
  12. lemma OAI.ArtinCAT0.mirrorReflect_next line 49
  13. lemma OAI.ArtinCAT0.mirrorReflect_prev line 50
  14. lemma OAI.ArtinCAT0.mirrorReflect_extra line 51
  15. lemma OAI.ArtinCAT0.mirrorReflect_extra_next line 52
  16. def OAI.ArtinCAT0.mirrorBasis line 54
  17. def OAI.ArtinCAT0.mirrorAut line 56
  18. lemma OAI.ArtinCAT0.mirrorAut_apply line 66
  19. lemma OAI.ArtinCAT0.mirrorAut_basis line 69
  20. abbrev OAI.ArtinCAT0.MirrorAffine line 75
  21. def OAI.ArtinCAT0.mirrorGenerator line 77
  22. lemma OAI.ArtinCAT0.mirrorGenerator_braid line 80
  23. def OAI.ArtinCAT0.mirrorRepresentation line 93
  24. lemma OAI.ArtinCAT0.mirrorRepresentation_gen line 96
  25. def OAI.ArtinCAT0.mirrorVector line 99
  26. def OAI.ArtinCAT0.mirrorLinear line 102
  27. lemma OAI.ArtinCAT0.mirrorVector_mul line 105
  28. lemma OAI.ArtinCAT0.mirrorVector_one line 109
  29. lemma OAI.ArtinCAT0.mirrorVector_generator_abs line 111