OAI/Combinatorics/SumProduct/Alignment/RationalTriangular01.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.AllLevelFactorization.Factorization line 35
  2. theorem OAI.AllLevelFactorization.factorization_exists line 55
  3. def OAI.AllLevelFactorization.Factorization.smoothPart line 107
  4. def OAI.AllLevelFactorization.Factorization.smoothLimit line 110
  5. def OAI.AllLevelFactorization.Factorization.structuredPart line 113
  6. lemma OAI.AllLevelFactorization.Factorization.quotient_mul_congr line 117
  7. theorem OAI.AllLevelFactorization.Factorization.realization line 125
  8. theorem OAI.AllLevelFactorization.Factorization.smooth_limit line 144
  9. theorem OAI.AllLevelFactorization.Factorization.smooth_bounds line 152
  10. theorem OAI.AllLevelFactorization.Factorization.limit_smooth line 159
  11. lemma OAI.RationalLattice.polynomialMap_realPower line 185
  12. lemma OAI.RationalLattice.polynomialMap_list_prod line 194
  13. lemma OAI.RationalLattice.axis_rational line 203
  14. theorem OAI.RationalLattice.rationalHom_polynomial line 212
  15. def OAI.RationalTriangularChange.forward line 257
  16. def OAI.RationalTriangularChange.inverse line 261
  17. lemma OAI.RationalTriangularChange.inverse_castSucc line 268
  18. lemma OAI.RationalTriangularChange.inverse_last line 273
  19. lemma OAI.RationalTriangularChange.forward_inverse line 279
  20. lemma OAI.RationalTriangularChange.forward_injective line 305
  21. lemma OAI.RationalTriangularChange.inverse_forward line 321
  22. lemma OAI.RationalTriangularChange.forward_polynomial line 325
  23. lemma OAI.RationalTriangularChange.inverse_polynomial line 330
  24. lemma OAI.RationalTriangularChange.polynomial_continuous line 344
  25. def OAI.RationalTriangularChange.homeomorph line 350