OAI/Combinatorics/BalancedRyser/Incidence/StabilityLeadingPart.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.StabilityPolynomial.homogeneousComponent_mul_of_degree_le line 13
  2. theorem OAI.Balanced.StabilityPolynomial.topHomogeneousComponent_ne_zero line 51
  3. def OAI.Balanced.StabilityPolynomial.dehomogenize line 63
  4. theorem OAI.Balanced.StabilityPolynomial.dehomogenize_ne_zero_of_homogeneous line 66
  5. theorem OAI.Balanced.StabilityPolynomial.natDegree_dehomogenize_le line 75
  6. def OAI.Balanced.StabilityPolynomial.leadingSpecialization line 95
  7. theorem OAI.Balanced.StabilityPolynomial.natDegree_leadingSpecialization_le line 98
  8. theorem OAI.Balanced.StabilityPolynomial.leadingSpecialization_ne_zero line 102
  9. theorem OAI.Balanced.StabilityPolynomial.leadingSpecialization_mul_of_degree_le line 107
  10. theorem OAI.Balanced.StabilityPolynomial.leadingSpecialization_redeiFactor line 115
  11. def OAI.Balanced.StabilityPolynomial.redeiLeadingProduct line 124
  12. theorem OAI.Balanced.StabilityPolynomial.leadingSpecialization_redeiPolynomial line 127
  13. theorem OAI.Balanced.StabilityPolynomial.homogeneousComponent_grid_term line 141
  14. theorem OAI.Balanced.StabilityPolynomial.leadingSpecialization_grid_term line 154
  15. theorem OAI.Balanced.StabilityPolynomial.redei_leading_identity line 161
  16. theorem OAI.Balanced.StabilityPolynomial.card_le_totalDegree_of_grid_vanishing line 184
  17. theorem OAI.Balanced.StabilityPolynomial.card_le_redei_auxiliary_degree line 198
  18. theorem OAI.Balanced.StabilityPolynomial.exists_redei_leading_identity line 207