OAI/Topology/ArtinGroups/Diagrams/Index.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.FiveBlock.Index line 10
2. def OAI.HarmonicArtin.FiveBlock.differential line 12
3. def OAI.HarmonicArtin.FiveBlock.projection line 27
4. def OAI.HarmonicArtin.FiveBlock.injection line 32
5. def OAI.HarmonicArtin.FiveBlock.homotopy line 37
6. def OAI.HarmonicArtin.FiveBlock.identity line 42
7. lemma OAI.HarmonicArtin.FiveBlock.contraction line 50