OAI/NumberTheory/PiExponent/Cohomology/MixedEulerAlgebra.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponent.NumericalAmpleness.LineIsoInvariant line 13
  2. def OAI.PiExponent.NumericalAmpleness.tensorDifference line 16
  3. def OAI.PiExponent.NumericalAmpleness.mixedDifference line 19
  4. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_nil line 23
  5. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_cons line 24
  6. def OAI.PiExponent.NumericalAmpleness.tensorTwistSwapIso line 28
  7. theorem OAI.PiExponent.NumericalAmpleness.tensorDifference_sub line 34
  8. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_sub line 40
  9. theorem OAI.PiExponent.NumericalAmpleness.tensorDifference_add line 46
  10. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_add line 52
  11. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_zero line 58
  12. theorem OAI.PiExponent.NumericalAmpleness.LineIsoInvariant.tensorDifference line 67
  13. theorem OAI.PiExponent.NumericalAmpleness.LineIsoInvariant.mixedDifference line 73
  14. theorem OAI.PiExponent.NumericalAmpleness.LineIsoInvariant.tensorShift line 79
  15. theorem OAI.PiExponent.NumericalAmpleness.LineIsoInvariant.pullback line 84
  16. theorem OAI.PiExponent.NumericalAmpleness.tensorDifference_commute line 89
  17. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_cons_commute line 97
  18. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_tensorShift line 108
  19. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_pullback line 119
  20. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_append line 133
  21. theorem OAI.PiExponent.NumericalAmpleness.tensorDifference_tensor line 139
  22. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_tensor_cons line 149
  23. theorem OAI.PiExponent.NumericalAmpleness.mixedDifference_tensor_cons_of_next_eq_zero line 156