OAI/NumberTheory/PiExponent/Cohomology/MixedEulerPolarization.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.NumericalAmpleness.structureLineBundle line 11
  2. def OAI.PiExponent.NumericalAmpleness.MixedDegreeLE line 16
  3. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_perm line 19
  4. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_iso_cons line 28
  5. theorem OAI.PiExponent.NumericalAmpleness.MixedDegreeLE.eq_zero_of_length_lt line 37
  6. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_tensor_base_of_degree line 49
  7. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_eq_structure_of_degree line 56
  8. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_tensor_cons_of_degree line 65
  9. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_pow_zero_cons line 75
  10. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_pow_cons_of_degree line 83
  11. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_replicate_pow line 94
  12. def OAI.PiExponent.NumericalAmpleness.mixedTop line 108
  13. theorem OAI.PiExponent.NumericalAmpleness.mixedTop_replicate line 111
  14. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_replicate_tensor_append line 118
  15. theorem OAI.PiExponent.NumericalAmpleness.mixedTop_tensor_binomial line 159
  16. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_replicate_pow_append line 168
  17. theorem OAI.PiExponent.NumericalAmpleness.mixedTop_two_powers line 187
  18. theorem OAI.PiExponent.NumericalAmpleness.mixedTop_tensor_powers_binomial line 203
  19. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_two_powers_append line 216
  20. theorem OAI.PiExponent.NumericalAmpleness.mixedTop_tensor_powers_binomial_append line 234