OAI/NumberTheory/PiExponent/Polynomials/AuxiliaryPolynomial.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.polynomialOfCoefficients line 12
2. theorem OAI.PiExponent.exponentVector_injective line 22
3. theorem OAI.PiExponent.polynomialOfCoefficients_coeff line 29
4. theorem OAI.PiExponent.polynomialOfCoefficients_injective line 47
5. theorem OAI.PiExponent.polynomialOfCoefficients_support line 55
6. theorem OAI.PiExponent.polynomialOfCoefficients_weighted line 73
7. theorem OAI.PiExponent.exists_nonzero_kernel_of_card_lt line 86
8. theorem OAI.PiExponent.tendsto_card_strictWeightedSimplex_scale line 94
9. theorem OAI.PiExponent.eventually_auxiliary_card_lt line 110
10. theorem OAI.PiExponent.eventually_exists_auxiliaryPolynomial line 138