OAI/NumberTheory/PiExponent/Cohomology/EulerPolynomialDegree.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PiExponent.NumericalAmpleness.iterate_fwdDiff_sub line 20
2. lemma OAI.PiExponent.NumericalAmpleness.difference_step line 25
3. theorem OAI.PiExponent.NumericalAmpleness.projective_line_cohomology_finite line 36
4. theorem OAI.PiExponent.NumericalAmpleness.euler_tensor_power_difference_aux line 47
5. theorem OAI.PiExponent.NumericalAmpleness.euler_tensor_power_difference_eq_zero line 121
6. theorem OAI.PiExponent.NumericalAmpleness.euler_power_difference_eq_zero line 133
7. theorem OAI.PiExponent.NumericalAmpleness.euler_tensor_power_dimension_difference_eq_zero line 147
8. theorem OAI.PiExponent.NumericalAmpleness.euler_power_dimension_difference_eq_zero line 166
9. theorem OAI.PiExponent.NumericalAmpleness.exists_euler_tensor_polynomial line 181
10. theorem OAI.PiExponent.NumericalAmpleness.exists_euler_polynomial line 193