OAI/Algebra/FinitisticAsymmetry/Augmentation/Directed.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.DirectedBound.DirectedSystem.Vertices line 16
2. def OAI.LittleFinitistic.DirectedBound.DirectedSystem.coefficient line 17
3. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.coefficient_spec line 18
4. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.coefficient_eq_iff line 20
5. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.corner_mul line 25
6. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.diagonal_mul line 32
7. def OAI.LittleFinitistic.DirectedBound.DirectedSystem.augmentation line 41
8. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.coefficient_vertex line 60
9. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.augmentation_surjective line 69
10. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.mem_augmentation_ker_iff line 76
11. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.ker_corner_vanish line 92
12. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.pow_ker_corner_vanish line 98
13. lemma OAI.LittleFinitistic.DirectedBound.DirectedSystem.augmentation_ker_nilpotent line 116