OAI/Combinatorics/SumProduct/Alignment/RationalFactor01.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubeFaces.Filtration.pullback line 23
  2. def OAI.CubeFaces.Filtration.refine line 35
  3. theorem OAI.CubePolynomials.pullback_mem line 66
  4. theorem OAI.CubePolynomials.refine_mem line 92
  5. theorem OAI.CubePolynomials.refine_of_linear_coset line 120
  6. lemma OAI.RationalFactorPeriods.eval_desc line 143
  7. lemma OAI.RationalFactorPeriods.choose_period_dvd line 151
  8. lemma OAI.RationalFactorPeriods.zpow_eq_of_sub_dvd line 164
  9. def OAI.RationalFactorPeriods.orderedWord line 172
  10. lemma OAI.RationalFactorPeriods.orderedWord_map line 175
  11. lemma OAI.RationalFactorPeriods.orderedWord_congr line 180
  12. lemma OAI.RationalFactorPeriods.orderedWord_periodic line 186
  13. lemma OAI.RationalFactorPeriods.finite_image_periodic line 196
  14. lemma OAI.RationalFactorPeriods.finite_image_stabilizes line 206
  15. lemma OAI.RationalFactorPeriods.coset_pattern_stabilizes line 223
  16. lemma OAI.RationalFactorPeriods.periodic_mod line 246
  17. theorem OAI.RationalFactorPeriods.rational_right_factors line 253