OAI/GroupTheory/FiniteType/TwistedBrinBasisMatching.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.TwistedBrin.Basis.Matching.near_cocycle_trivial line 24
  2. theorem OAI.TwistedBrin.Basis.CutDown.cocycle_trivial_high_rank line 52
  3. theorem OAI.TwistedBrin.Basis.CutBasis.sublevel_cocycle_trivial line 81
  4. structure OAI.ActionTransport.Gauge line 104
  5. theorem OAI.ActionTransport.section_of_cocycle line 110
  6. class OAI.ActionTransport.IsMonotoneAction line 173
  7. structure OAI.ActionTransport.Frames line 176
  8. def OAI.ActionTransport.Frames.stab line 187
  9. lemma OAI.ActionTransport.Frames.mem_stab line 188
  10. lemma OAI.ActionTransport.Frames.difference_mem line 189
  11. lemma OAI.ActionTransport.Frames.difference line 194
  12. lemma OAI.ActionTransport.act_mono line 200
  13. def OAI.ActionTransport.Edge line 202
  14. instance OAI.ActionTransport.Edge.(instance at line 204) line 204
  15. lemma OAI.ActionTransport.Edge.fst_smul line 214
  16. lemma OAI.ActionTransport.Edge.snd_smul line 215
  17. lemma OAI.ActionTransport.eq_top_of_frames line 218
  18. lemma OAI.ActionTransport.fg_of_frames line 258
  19. structure OAI.ActionTransport.LiftedFrames line 287
  20. def OAI.ActionTransport.LiftedFrames.eval line 292
  21. lemma OAI.ActionTransport.LiftedFrames.eval_valid line 296
  22. lemma OAI.ActionTransport.LiftedFrames.eval_one line 300
  23. lemma OAI.ActionTransport.LiftedFrames.eval_mul line 303
  24. lemma OAI.ActionTransport.LiftedFrames.eval_projects line 307
  25. def OAI.ActionTransport.LiftedFrames.gauge line 310
  26. def OAI.ActionTransport.edgeTransport line 326
  27. def OAI.ActionTransport.rawEdge line 329
  28. lemma OAI.ActionTransport.rawEdge_projects line 333
  29. lemma OAI.ActionTransport.edgeTransport_stabilizer line 344
  30. lemma OAI.ActionTransport.rawEdge_equivariant line 358
  31. def OAI.ActionTransport.Gauge.map line 385
  32. def OAI.ActionTransport.Edge.diag line 393
  33. lemma OAI.ActionTransport.Edge.diag_smul line 394
  34. def OAI.ActionTransport.Triangle line 397
  35. instance OAI.ActionTransport.Triangle.(instance at line 400) line 400
  36. def OAI.ActionTransport.Triangle.e01 line 412
  37. def OAI.ActionTransport.Triangle.e12 line 413
  38. def OAI.ActionTransport.Triangle.e02 line 414
  39. lemma OAI.ActionTransport.Triangle.e01_smul line 415
  40. lemma OAI.ActionTransport.Triangle.e12_smul line 416
  41. lemma OAI.ActionTransport.Triangle.e02_smul line 417
  42. lemma OAI.ActionTransport.flat_triangle_translate line 420
  43. def OAI.ActionTransport.cocycleOfFlat line 432
  44. lemma OAI.ActionTransport.rawEdge_map line 449