OAI/Topology/ArtinGroups/Complexes/InverseMatrix.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_homotopy_degree11 line 18
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_homotopy_degree22 line 30
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_homotopy_degree21 line 37
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.through_absent_level_zero line 49
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_identity_blocks line 66
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_homotopy_source_block line 75
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_homotopy_target_block line 91
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_layer_inverse_equations line 107
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.inverseMatrix line 175
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.coneLayerIsomorphism line 195
11. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayer_eq_of_cone_gap line 215