OAI/NumberTheory/PiExponent/Cohomology/MixedEulerTop.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.NumericalAmpleness.topEuler line 12
2. def OAI.PiExponent.NumericalAmpleness.mixedEuler line 15
3. theorem OAI.PiExponent.NumericalAmpleness.mixedEuler_replicate line 18
4. theorem OAI.PiExponent.NumericalAmpleness.mixedEuler_perm line 22
5. theorem OAI.PiExponent.NumericalAmpleness.lineEuler_mixedDegreeLE line 27
6. theorem OAI.PiExponent.NumericalAmpleness.mixedEuler_tensor_cons line 33
7. theorem OAI.PiExponent.NumericalAmpleness.topEuler_pow line 42
8. theorem OAI.PiExponent.NumericalAmpleness.topEuler_tensor_powers_binomial line 52
9. theorem OAI.PiExponent.NumericalAmpleness.mixedEuler_tensor_powers_binomial_append line 63