OAI/RingTheory/BassTrace/FreeParameters.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BassTrace.FreeParameter.residue line 20
  2. lemma OAI.BassTrace.FreeParameter.residue_out line 25
  3. lemma OAI.BassTrace.FreeParameter.residue_mul line 29
  4. lemma OAI.BassTrace.FreeParameter.out_mul_residue line 33
  5. abbrev OAI.BassTrace.FreeParameter.Offsets line 39
  6. def OAI.BassTrace.FreeParameter.encode line 41
  7. lemma OAI.BassTrace.FreeParameter.encode_out line 44
  8. lemma OAI.BassTrace.FreeParameter.encode_mul line 48
  9. lemma OAI.BassTrace.FreeParameter.encode_injective line 52
  10. def OAI.BassTrace.FreeParameter.shift line 57
  11. lemma OAI.BassTrace.FreeParameter.encode_shift line 60
  12. lemma OAI.BassTrace.FreeParameter.shift_one line 66
  13. lemma OAI.BassTrace.FreeParameter.shift_mul line 71
  14. lemma OAI.BassTrace.FreeParameter.shift_not_fixed line 77
  15. lemma OAI.BassTrace.FreeParameter.continuous_shift line 87
  16. lemma OAI.BassTrace.FreeParameter.measurable_shift line 93
  17. def OAI.BassTrace.FreeParameter.uniform line 103
  18. instance OAI.BassTrace.FreeParameter.uniform_probability line 105
  19. lemma OAI.BassTrace.FreeParameter.uniform_map_equiv line 109
  20. def OAI.BassTrace.FreeParameter.offsetMeasure line 124
  21. instance OAI.BassTrace.FreeParameter.offsetMeasure_probability line 127
  22. lemma OAI.BassTrace.FreeParameter.reindex_measure line 132
  23. lemma OAI.BassTrace.FreeParameter.offsetMeasure_shift line 142
  24. structure OAI.BassTrace.FreeParameter.Character line 167
  25. lemma OAI.BassTrace.FreeParameter.zpowers_subtype_generator line 176
  26. def OAI.BassTrace.FreeParameter.character line 186
  27. instance OAI.BassTrace.FreeParameter.Character.colorTopology line 217
  28. instance OAI.BassTrace.FreeParameter.Character.colorDiscrete line 219
  29. instance OAI.BassTrace.FreeParameter.Character.colorMeasurable line 221
  30. instance OAI.BassTrace.FreeParameter.Character.colorSingleton line 223
  31. instance OAI.BassTrace.FreeParameter.Character.colorBorel line 225
  32. instance OAI.BassTrace.FreeParameter.Character.colorFintype line 227
  33. abbrev OAI.BassTrace.FreeParameter.Space line 233
  34. instance OAI.BassTrace.FreeParameter.spaceTopology line 236
  35. instance OAI.BassTrace.FreeParameter.spaceMeasurable line 240
  36. instance OAI.BassTrace.FreeParameter.spaceCompact line 244
  37. instance OAI.BassTrace.FreeParameter.spaceT2 line 248
  38. instance OAI.BassTrace.FreeParameter.spaceTotallyDisconnected line 252
  39. instance OAI.BassTrace.FreeParameter.quotientCountable line 256
  40. instance OAI.BassTrace.FreeParameter.spaceMetrizable line 259
  41. instance OAI.BassTrace.FreeParameter.spaceBorel line 263
  42. instance OAI.BassTrace.FreeParameter.spaceAction line 267
  43. instance OAI.BassTrace.FreeParameter.spaceContinuous line 272
  44. instance OAI.BassTrace.FreeParameter.spaceFree line 278
  45. def OAI.BassTrace.FreeParameter.probability line 286
  46. instance OAI.BassTrace.FreeParameter.probability_isProbability line 290
  47. lemma OAI.BassTrace.FreeParameter.probability_preserving line 297