OAI/NumberTheory/PowerFree/ResidueBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.QuarticPowerFree.separate_powers_normal_form line 17
2. theorem OAI.QuarticPowerFree.card_separate_powers_roots line 53
3. theorem OAI.QuarticPowerFree.card_nonsingular_polynomial_roots line 99
4. theorem OAI.QuarticPowerFree.totalDegree_linear_substitute_le line 140
5. def OAI.QuarticPowerFree.partialEval line 160
6. theorem OAI.QuarticPowerFree.eval_partialEval line 164
7. theorem OAI.QuarticPowerFree.totalDegree_partialEval_le line 175
8. theorem OAI.QuarticPowerFree.pderiv_partialEval line 186
9. theorem OAI.QuarticPowerFree.card_smooth_patch line 202
10. theorem OAI.QuarticPowerFree.card_regular_residue_tuples line 239