OAI/GroupTheory/FiniteType/TwistedBrinBasisCutBasis.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.TwistedBrin.Basis.CutBasis.(instance at line 20) line 20
  2. lemma OAI.TwistedBrin.Basis.CutBasis.smul_val line 24
  3. instance OAI.TwistedBrin.Basis.CutBasis.(instance at line 25) line 25
  4. abbrev OAI.TwistedBrin.Basis.CutBasis.Sublevel line 27
  5. instance OAI.TwistedBrin.Basis.CutBasis.(instance at line 28) line 28
  6. instance OAI.TwistedBrin.Basis.CutBasis.(instance at line 35) line 35
  7. lemma OAI.TwistedBrin.Basis.CutBasis.sublevel_val_injective line 37
  8. lemma OAI.TwistedBrin.Basis.CutBasis.vertex_finite_orbits line 40
  9. lemma OAI.TwistedBrin.Basis.CutBasis.edge_finite_orbits line 49
  10. lemma OAI.TwistedBrin.Basis.CutBasis.triangle_finite_orbits line 62
  11. lemma OAI.TwistedBrin.Basis.CutBasis.sublevel_connected line 86
  12. lemma OAI.FiniteExtension.finitelyGenerated line 102
  13. lemma OAI.TwistedBrin.Basis.vertex_finitelyPresented line 126
  14. lemma OAI.TwistedBrin.Basis.pair_finitelyGenerated line 132
  15. lemma OAI.TwistedBrin.Basis.CutBasis.sublevel_vertex_stabilizer line 146
  16. lemma OAI.TwistedBrin.Basis.CutBasis.sublevel_edge_stabilizer line 152
  17. theorem OAI.TwistedBrin.Basis.CutBasis.localGroup_finitelyPresented line 162
  18. def OAI.OrderChainComplex.simplexSet line 192
  19. def OAI.OrderChainComplex.chains line 193
  20. lemma OAI.OrderChainComplex.mem_chains line 195
  21. def OAI.OrderChainComplex.basisIso line 203
  22. instance OAI.OrderChainComplex.(instance at line 206) line 206
  23. lemma OAI.OrderChainComplex.boundary_internal line 208
  24. def OAI.OrderChainComplex.d line 212
  25. def OAI.OrderChainComplex.aug line 214
  26. lemma OAI.OrderChainComplex.d_val line 215
  27. lemma OAI.OrderChainComplex.d_d line 216
  28. lemma OAI.OrderChainComplex.d_aug line 221
  29. lemma OAI.OrderChainComplex.augmentation_degree line 225
  30. lemma OAI.OrderChainComplex.aug_surjective line 237
  31. lemma OAI.OrderChainComplex.exact_aug line 245
  32. lemma OAI.OrderChainComplex.exact_succ line 264