OAI/Geometry/PeriodicTiling/RationalPolynomialPeriod.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PeriodicTilingThree.finite_common_denominator line 18
2. theorem OAI.PeriodicTilingThree.circle_eval_eq_sum line 37
3. theorem OAI.PeriodicTilingThree.circle_monomial_add_period line 44
4. theorem OAI.PeriodicTilingThree.rational_nonconstant_circlePolynomial_periodic line 61
5. theorem OAI.PeriodicTilingThree.circle_monomial_scaled_eq_zero line 79
6. theorem OAI.PeriodicTilingThree.exists_progression_irrational_leadingCoeff line 95