OAI/NumberTheory/SiegelZeros/Structure/KoszulDualStep.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SiegelZeros.SiegelZerosAwei.W30.coneBottom_comp line 19
  2. def OAI.SiegelZeros.SiegelZerosAwei.W30.scalarConeObject line 29
  3. def OAI.SiegelZeros.SiegelZerosAwei.W30.scalarConeMap line 33
  4. lemma OAI.SiegelZeros.SiegelZerosAwei.W30.chain_linear_comp_zero line 39
  5. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarConeMap_comp line 44
  6. def OAI.SiegelZeros.SiegelZerosAwei.W30.scalarConeComplex line 55
  7. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_interior_exact line 59
  8. def OAI.SiegelZeros.SiegelZerosAwei.W30.dualConeDifferential line 82
  9. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.dualConeDifferential_apply line 87
  10. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneDifferential_dual_precomposition line 91
  11. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneDifferential_dual_equiv line 103
  12. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.dualConeDifferential_exact line 110
  13. def OAI.SiegelZeros.SiegelZerosAwei.W30.emptyKoszulObject line 159
  14. def OAI.SiegelZeros.SiegelZerosAwei.W30.emptyKoszulComplex line 163
  15. def OAI.SiegelZeros.SiegelZerosAwei.W30.iterateScalarCones line 166
  16. def OAI.SiegelZeros.SiegelZerosAwei.W30.regularSequenceComplex line 171
  17. lemma OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_free line 174
  18. lemma OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_finite line 185
  19. lemma OAI.SiegelZeros.SiegelZerosAwei.W30.iterateScalarCones_free line 196
  20. lemma OAI.SiegelZeros.SiegelZerosAwei.W30.iterateScalarCones_finite line 203
  21. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.regularSequenceComplex_free line 210
  22. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.regularSequenceComplex_finite line 222
  23. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.dualCone_endpoint_exact line 248
  24. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.exact_of_equivalences line 306
  25. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_dual_interior_exact line 342
  26. def OAI.SiegelZeros.SiegelZerosAwei.W30.dualConeBottom line 381
  27. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.dualConeBottom_apply line 385
  28. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.coneBottom_dual_equiv line 388
  29. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.dualConeBottom_exact line 398
  30. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.dualConeBottom_injective line 424
  31. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.dualConeBottom_injective_of_regular line 429
  32. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.dualConeBottom_endpoint_exact line 434
  33. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_dual_one_exact line 470
  34. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.chain_dual_comp_zero line 505
  35. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_dual_endpoint_exact line 516
  36. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_dual_one_endpoint_exact line 545
  37. theorem OAI.SiegelZeros.SiegelZerosAwei.W30.scalarCone_dual_low_exact line 572