OAI/Combinatorics/BalancedRyser/Local/AlignedGlobalProduct.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.Local.AlignedGlobal.FreeIndex line 17
  2. abbrev OAI.Balanced.Local.AlignedGlobal.AlignedOffsets line 20
  3. def OAI.Balanced.Local.AlignedGlobal.coordinates line 24
  4. theorem OAI.Balanced.Local.AlignedGlobal.tuple_offsets_eq_of_points line 34
  5. theorem OAI.Balanced.Local.AlignedGlobal.coordinates_injective line 46
  6. def OAI.Balanced.Local.AlignedGlobal.coordinateEquiv line 108
  7. theorem OAI.Balanced.Local.AlignedGlobal.coordinateEquiv_apply line 117
  8. theorem OAI.Balanced.Local.AlignedGlobal.generated_free line 123
  9. theorem OAI.Balanced.Local.AlignedGlobal.generated_unused line 137
  10. theorem OAI.Balanced.Local.AlignedGlobal.alignedLaw_eq_uniform_coordinates line 146
  11. theorem OAI.Balanced.Local.AlignedGlobal.conditioned_probability_eq_uniform_coordinates line 164