OAI/Geometry/SingularHomology/SingularChainsFinsuppBoundary.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.SingularChainFormulas.simplexChain line 15
2. def OAI.Problem340.SingularChainFormulas.face line 20
3. lemma OAI.Problem340.SingularChainFormulas.simplexChain_boundary line 24
4. lemma OAI.Problem340.SingularChainFormulas.simplexChain_boundary_real line 40
5. lemma OAI.Problem340.SingularChainFormulas.simplexChain_map line 47
6. abbrev OAI.Problem340.realSingularFace line 66
7. lemma OAI.Problem340.realSingularGenerator_eq_smul line 70
8. lemma OAI.Problem340.realSingularGenerator_boundary line 75
9. lemma OAI.Problem340.realSingularGenerator_map line 85
10. def OAI.Problem340.realSingularBoundary line 92
11. def OAI.Problem340.realSingularPushforward line 97
12. lemma OAI.Problem340.realSingularBoundary_single line 102
13. lemma OAI.Problem340.realSingularPushforward_single line 108
14. lemma OAI.Problem340.singularChainsFinsuppEquiv_boundary line 113
15. lemma OAI.Problem340.singularChainsFinsuppEquiv_pushforward line 134
16. lemma OAI.Problem340.realSingularBoundary_squared line 153
17. lemma OAI.Problem340.realSingularBoundary_pushforward line 163