OAI/Combinatorics/Progressions/Polynomial/PolynomialDifferencePermanentBlocks.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.permanentPolynomial line 13
  2. def OAI.Erdos3.permanentExponent line 16
  3. theorem OAI.Erdos3.permanentExponent_apply line 19
  4. theorem OAI.Erdos3.permanentExponent_injective line 26
  5. theorem OAI.Erdos3.permanentPolynomial_eq_monomial_sum line 36
  6. theorem OAI.Erdos3.permanentPolynomial_degreeOf line 44
  7. theorem OAI.Erdos3.permanentPolynomial_totalDegree line 58
  8. theorem OAI.Erdos3.permanentPolynomial_coeff line 71
  9. theorem OAI.Erdos3.permanentExponent_one_eq_diagonal line 77
  10. theorem OAI.Erdos3.permanentPolynomial_diagonal_coefficient line 82
  11. theorem OAI.Erdos3.eval_permanentPolynomial line 88
  12. theorem OAI.Erdos3.permanent_gcd_mean_sublevel line 101
  13. theorem OAI.Erdos3.permanent_zero_gcd_mean line 113
  14. theorem OAI.Erdos3.permanent_gcd_mean_sublevel_all line 127
  15. theorem OAI.Erdos3.disjoint_permanent_gcd_mean_bound line 148
  16. theorem OAI.Erdos3.disjoint_permanent_gcd_mean_bound_curried line 168
  17. theorem OAI.Erdos3.disjoint_permanent_gcd_mean_bound_all line 191
  18. theorem OAI.Erdos3.disjoint_permanent_gcd_mean_bound_curried_all line 211