OAI/Combinatorics/SumProduct/Alignment/PivotPaths03.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SourcePivotPaths.scaleRun_pos line 28
  2. lemma OAI.SourcePivotPaths.sourcePlan_positive line 38
  3. lemma OAI.SourcePivotPaths.source_multipliers_pos line 43
  4. def OAI.SourcePivotPaths.nextScales line 58
  5. lemma OAI.SourcePivotPaths.mem_nextScales line 62
  6. lemma OAI.SourcePivotPaths.nextScales_pos line 68
  7. def OAI.SourcePivotPaths.planModulus line 78
  8. lemma OAI.SourcePivotPaths.terminalDenom_pos line 85
  9. lemma OAI.SourcePivotPaths.planModulus_pos line 89
  10. lemma OAI.SourcePivotPaths.planModulus_head line 97
  11. lemma OAI.SourcePivotPaths.planModulus_terminal line 101
  12. lemma OAI.SourcePivotPaths.planModulus_tail line 106
  13. structure OAI.SourceChartedAlignment.CommonScales line 131
  14. structure OAI.SourceChartedAlignment.PivotScales line 152
  15. structure OAI.SourceChartedAlignment.ChartedModels line 168
  16. def OAI.SourceChartedAlignment.CommonScales.law line 203
  17. instance OAI.SourceChartedAlignment.(instance at line 206) line 206
  18. def OAI.SourceChartedAlignment.ChartedModels.scalar line 210
  19. def OAI.SourceProductCoordinates.homeomorph line 234
  20. def OAI.SourceProductCoordinates.lower line 253
  21. lemma OAI.SourceProductCoordinates.homeomorph_lower line 258
  22. def OAI.SourceProductCoordinates.coordinates line 266
  23. def OAI.SourceProductCoordinates.select line 283
  24. lemma OAI.SourceProductCoordinates.select_some_iff line 286
  25. lemma OAI.SourceProductCoordinates.select_enumeration line 305
  26. lemma OAI.SourceProductCoordinates.axis_selected line 325
  27. lemma OAI.SourceProductCoordinates.axis_other line 342
  28. lemma OAI.SourceProductCoordinates.prod_select line 354
  29. theorem OAI.SourceProductCoordinates.secondKind line 367