OAI/Combinatorics/SumProduct/Alignment/IntegerArrays12.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.centerAV line 23
  2. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.terminalAV line 25
  3. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.required line 30
  4. abbrev OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.Index line 33
  5. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.formula line 35
  6. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.coefficient line 45
  7. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.residue line 46
  8. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.slotSum line 48
  9. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.compile line 50
  10. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.scalar line 52
  11. def OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.numericSuccess line 56
  12. lemma OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.center_mem line 67
  13. lemma OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.terminal_mem line 73
  14. lemma OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.formula_val line 79
  15. lemma OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.terminal_support line 84
  16. lemma OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.input_pairing line 107
  17. lemma OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.slotSum_add line 130
  18. lemma OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.compile_value line 135
  19. lemma OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.numeric_shift line 148
  20. theorem OAI.SourceIntegerArrays.GlobalJoint.FiniteModelSlots.source_numeric_success line 183
  21. def OAI.SourceIntegerArrays.GlobalJoint.SourceExposureSlots.qValue line 230
  22. def OAI.SourceIntegerArrays.GlobalJoint.SourceExposureSlots.tailValue line 232
  23. def OAI.SourceIntegerArrays.GlobalJoint.SourceExposureSlots.rValue line 234
  24. def OAI.SourceIntegerArrays.GlobalJoint.SourceExposureSlots.slotValue line 236
  25. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceExposureSlots.coprime_mod_congr line 239
  26. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceExposureSlots.residue_congr line 246
  27. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceExposureSlots.residue_dvd line 254
  28. theorem OAI.SourceIntegerArrays.GlobalJoint.SourceExposureSlots.source_exposure_slots line 272