OAI/Topology/ArtinGroups/Diagrams/Relation.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.HarmonicArtin.TemperleyLieb.Relation line 12
2. abbrev OAI.HarmonicArtin.TemperleyLieb.Algebra line 25
3. def OAI.HarmonicArtin.TemperleyLieb.generator line 27
4. lemma OAI.HarmonicArtin.TemperleyLieb.generator_square line 30
5. lemma OAI.HarmonicArtin.TemperleyLieb.generator_adjacent line 35
6. lemma OAI.HarmonicArtin.TemperleyLieb.generator_adjacent_rev line 40
7. lemma OAI.HarmonicArtin.TemperleyLieb.generator_distant line 45
8. lemma OAI.HarmonicArtin.TemperleyLieb.sandwich_step line 54
9. lemma OAI.HarmonicArtin.TemperleyLieb.projector_step line 73
10. def OAI.HarmonicArtin.TemperleyLieb.projector line 107
11. lemma OAI.HarmonicArtin.TemperleyLieb.projector_commute line 112
12. lemma OAI.HarmonicArtin.TemperleyLieb.projector_absorb line 121
13. lemma OAI.HarmonicArtin.TemperleyLieb.projector_properties line 131
14. def OAI.HarmonicArtin.TemperleyLieb.augmentation line 180
15. lemma OAI.HarmonicArtin.TemperleyLieb.augmentation_generator line 185
16. lemma OAI.HarmonicArtin.TemperleyLieb.augmentation_projector line 190
17. lemma OAI.HarmonicArtin.TemperleyLieb.projector_ne_zero line 196
18. def OAI.HarmonicArtin.TemperleyLieb.strands line 203
19. lemma OAI.HarmonicArtin.TemperleyLieb.strands_mono line 206
20. lemma OAI.HarmonicArtin.TemperleyLieb.generator_mem_strands line 210
21. lemma OAI.HarmonicArtin.TemperleyLieb.projector_mem_strands line 214
22. lemma OAI.HarmonicArtin.TemperleyLieb.turnback_scalar_action line 224
23. lemma OAI.HarmonicArtin.TemperleyLieb.turnback_projector_unique line 242