OAI/Combinatorics/SumProduct/Alignment/IntegerArrays14.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ConstructedWordPlan.GlobalWordPlan.SourceTerminalArithmetic.height line 15
  2. def OAI.ConstructedWordPlan.GlobalWordPlan.SourceTerminalArithmetic.coefficient line 18
  3. lemma OAI.ConstructedWordPlan.GlobalWordPlan.SourceTerminalArithmetic.pairing line 21
  4. lemma OAI.ConstructedWordPlan.GlobalWordPlan.SourceTerminalArithmetic.coefficient_exact line 46
  5. theorem OAI.ConstructedWordPlan.GlobalWordPlan.SourceTerminalArithmetic.source_terminal_arithmetic line 74
  6. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.heightCoeff line 140
  7. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.readOriginal line 142
  8. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.outcomeScales line 145
  9. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.terminalDenom line 147
  10. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.slots line 149
  11. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.pivotProperty line 153
  12. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reading_inner_product line 168
  13. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reading_coprime_mod line 180
  14. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reading_residue_congr line 186
  15. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reading_slotSum line 193
  16. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reading_slot_bound line 223
  17. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reading_scaleRun_pos line 237
  18. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reading_av_mem line 245
  19. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reading_scalar line 250
  20. theorem OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_pivot_reading line 262