OAI/Combinatorics/BalancedRyser/Incidence/StabilityLargeFiber.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Balanced.StabilityPolynomial.rootMultiplicity_linear_product line 13
2. theorem OAI.Balanced.StabilityPolynomial.rootMultiplicity_le_natDegree line 30
3. theorem OAI.Balanced.StabilityPolynomial.power_dvd_linear_product_card_bound line 35
4. theorem OAI.Balanced.StabilityPolynomial.large_fiber_of_power_dvd line 47
5. theorem OAI.Balanced.StabilityPolynomial.linear_pow_card line 57
6. theorem OAI.Balanced.StabilityPolynomial.frobenius_linear_factorization line 64
7. theorem OAI.Balanced.StabilityPolynomial.large_fiber_of_frobenius_divisor line 72
8. theorem OAI.Balanced.StabilityPolynomial.redei_large_vertical_fiber line 92