OAI/Combinatorics/SumProduct/Alignment/RationalLattice12.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RationalLattice.IsRealPolynomialMap line 30
  2. lemma OAI.RationalLattice.realPolynomialMap_one line 34
  3. lemma OAI.RationalLattice.realPolynomialMap_mul line 39
  4. lemma OAI.RationalLattice.realPolynomialMap_list_prod line 53
  5. lemma OAI.RationalLattice.realPolynomialMap_realPower line 62
  6. lemma OAI.RationalLattice.map_realPower line 69
  7. theorem OAI.RationalLattice.realHom_polynomial line 81
  8. def OAI.RationalLattice.logHom line 108
  9. lemma OAI.RationalLattice.logHom_polynomial line 111
  10. lemma OAI.RationalLattice.logHom_smul line 123
  11. lemma OAI.RationalLattice.logHom_contDiff line 127
  12. def OAI.RationalLattice.logHomLinear line 131
  13. lemma OAI.RationalLattice.logHomLinear_apply line 134
  14. lemma OAI.RationalLattice.map_canonicalExp line 140
  15. lemma OAI.RationalLattice.logHomLinear_log line 144
  16. def OAI.RoughKernelFactorization.sectionFlow line 168
  17. lemma OAI.RoughKernelFactorization.sectionFlow_continuous line 174
  18. lemma OAI.RoughKernelFactorization.sectionFlow_character line 179
  19. lemma OAI.RoughKernelFactorization.sectionFlow_rational line 189
  20. lemma OAI.RoughKernelFactorization.sectionFlow_polynomial line 200
  21. lemma OAI.RoughKernelFactorization.sectionFlow_exponential line 211
  22. lemma OAI.RoughKernelFactorization.sectionFlow_period line 223
  23. lemma OAI.RoughKernelFactorization.same_coset_of_mod line 244
  24. lemma OAI.RoughKernelFactorization.residual_mem line 271
  25. def OAI.RoughKernelFactorization.residual line 282
  26. lemma OAI.RoughKernelFactorization.residual_factorization line 287
  27. lemma OAI.RoughKernelFactorization.residual_polynomial line 299