OAI/Topology/ArtinGroups/Diagrams/ReverseDifferential.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.FiveBlock.reverseDifferentialline 10 - def
OAI.HarmonicArtin.FiveBlock.reverseProjectionline 25 - def
OAI.HarmonicArtin.FiveBlock.reverseInjectionline 30 - def
OAI.HarmonicArtin.FiveBlock.reverseHomotopyline 35 - lemma
OAI.HarmonicArtin.FiveBlock.reverseContractionline 40