OAI/Analysis/FreeGroupFactor/SmallCocycle.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FreeGroupFactorMain.coefficientNorm line 14
  2. theorem OAI.FreeGroupFactorMain.freeCocycle_pow_of_zero line 17
  3. def OAI.FreeGroupFactorMain.firstCoefficients line 24
  4. def OAI.FreeGroupFactorMain.sourceA line 27
  5. def OAI.FreeGroupFactorMain.sourceB line 30
  6. def OAI.FreeGroupFactorMain.sourcePrefix line 34
  7. def OAI.FreeGroupFactorMain.sourceWord line 38
  8. theorem OAI.FreeGroupFactorMain.freeCocycle_sourceA line 41
  9. theorem OAI.FreeGroupFactorMain.freeCocycle_sourceB line 46
  10. theorem OAI.FreeGroupFactorMain.freeCocycle_sourcePrefix line 55
  11. theorem OAI.FreeGroupFactorMain.freeCocycle_sourceWord line 65
  12. def OAI.FreeGroupFactorMain.PrefixSeparation.integerAction line 74
  13. abbrev OAI.FreeGroupFactorMain.PrefixSeparation.Witness line 87
  14. theorem OAI.FreeGroupFactorMain.PrefixSeparation.integerAction_of line 89
  15. def OAI.FreeGroupFactorMain.PrefixSeparation.witnessHom line 93
  16. theorem OAI.FreeGroupFactorMain.PrefixSeparation.witnessHom_sourceA line 98
  17. theorem OAI.FreeGroupFactorMain.PrefixSeparation.witnessHom_sourceB line 102
  18. def OAI.FreeGroupFactorMain.PrefixSeparation.integerPrefix line 109
  19. theorem OAI.FreeGroupFactorMain.PrefixSeparation.witnessHom_sourcePrefix line 113
  20. def OAI.FreeGroupFactorMain.PrefixSeparation.prefixHom line 119
  21. def OAI.FreeGroupFactorMain.PrefixSeparation.targetPrefix line 122
  22. theorem OAI.FreeGroupFactorMain.PrefixSeparation.targetPrefix_zero line 125
  23. theorem OAI.FreeGroupFactorMain.PrefixSeparation.targetPrefix_generator line 128
  24. def OAI.FreeGroupFactorMain.PrefixSeparation.telescopeHom line 132
  25. theorem OAI.FreeGroupFactorMain.PrefixSeparation.telescopeHom_integerPrefix line 135
  26. theorem OAI.FreeGroupFactorMain.PrefixSeparation.witnessHom_prefixHom line 143
  27. theorem OAI.FreeGroupFactorMain.PrefixSeparation.telescope_leftInverse line 151
  28. theorem OAI.FreeGroupFactorMain.PrefixSeparation.prefixHom_injective line 157
  29. def OAI.FreeGroupFactorMain.pushCoefficients line 172
  30. theorem OAI.FreeGroupFactorMain.pushCoefficients_single line 175
  31. theorem OAI.FreeGroupFactorMain.coefficientShift_single line 180
  32. theorem OAI.FreeGroupFactorMain.pushCoefficients_shift line 184
  33. theorem OAI.FreeGroupFactorMain.sqNorm_pushCoefficients line 192
  34. theorem OAI.FreeGroupFactorMain.cocycle_push_prefix_inverse line 197
  35. theorem OAI.FreeGroupFactorMain.smallCocycle line 213