OAI/NumberTheory/SiegelZeros/Structure/RectangleGenerators.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.Result.Workers.W57.iter line 26
  2. theorem OAI.SiegelZeros.Result.Workers.W57.iter_zero line 28
  3. theorem OAI.SiegelZeros.Result.Workers.W57.iter_succ line 29
  4. theorem OAI.SiegelZeros.Result.Workers.W57.iter_mul line 40
  5. theorem OAI.SiegelZeros.Result.Workers.W57.factorial_normalize line 56
  6. def OAI.SiegelZeros.Result.Workers.W57.taylorSeries line 70
  7. theorem OAI.SiegelZeros.Result.Workers.W57.coeff_taylorSeries line 73
  8. theorem OAI.SiegelZeros.Result.Workers.W57.taylorSeries_mul line 77
  9. def OAI.SiegelZeros.Result.Workers.W57.taylorHom line 88
  10. theorem OAI.SiegelZeros.Result.Workers.W57.coeff_taylorHom line 104
  11. theorem OAI.SiegelZeros.Result.Workers.W57.constantCoeff_taylorHom line 108
  12. def OAI.SiegelZeros.Result.Workers.W57.taylorHom₃ line 113
  13. theorem OAI.SiegelZeros.Result.Workers.W57.coeff_taylorHom₃ line 118
  14. theorem OAI.SiegelZeros.Result.Workers.W57.iter_commute line 126
  15. abbrev OAI.SiegelZeros.Result.Workers.W57.Series₃ line 131
  16. def OAI.SiegelZeros.Result.Workers.W57.coordinate line 135
  17. def OAI.SiegelZeros.Result.Workers.W57.rectangleIdeal line 140
  18. abbrev OAI.SiegelZeros.Result.Workers.W57.Rectangle line 143
  19. def OAI.SiegelZeros.Result.Workers.W57.rectangleTaylor line 145
  20. theorem OAI.SiegelZeros.Result.Workers.W57.coordinate_pow_eq_zero line 151
  21. def OAI.SiegelZeros.Result.Workers.W57.truncationIdeal line 158
  22. theorem OAI.SiegelZeros.Result.Workers.W57.truncation_eq_zero_iff line 161
  23. theorem OAI.SiegelZeros.Result.Workers.W57.taylor_truncation_eq_zero line 169
  24. abbrev OAI.SiegelZeros.Result.Workers.W57.Jet line 185
  25. instance OAI.SiegelZeros.Result.Workers.W57.jetCommRing line 187
  26. instance OAI.SiegelZeros.Result.Workers.W57.jetAlgebra line 190
  27. def OAI.SiegelZeros.Result.Workers.W57.jetProjection line 194
  28. abbrev OAI.SiegelZeros.Result.Workers.W57.RectangleJet line 197
  29. instance OAI.SiegelZeros.Result.Workers.W57.rectangleJetCommRing line 199
  30. instance OAI.SiegelZeros.Result.Workers.W57.rectangleJetAlgebra line 202
  31. def OAI.SiegelZeros.Result.Workers.W57.rectangleProjection line 206
  32. theorem OAI.SiegelZeros.Result.Workers.W57.rectangleProjection_eq_zero_iff line 211
  33. def OAI.SiegelZeros.Result.Workers.W57.rectangularJetHom line 220
  34. theorem OAI.SiegelZeros.Result.Workers.W57.rectangularJetHom_eq_zero line 226
  35. theorem OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant_comp line 252
  36. theorem OAI.SiegelZeros.WeightedTorusJets.W19.rectangle_index_add_bound line 264
  37. def OAI.SiegelZeros.WeightedTorusJets.W19.derivativeTriple line 277
  38. theorem OAI.SiegelZeros.WeightedTorusJets.W19.iter_add_apply line 280
  39. theorem OAI.SiegelZeros.WeightedTorusJets.W19.derivativeTriple_comp line 284
  40. def OAI.SiegelZeros.WeightedTorusJets.W19.rectangleGenerators line 294
  41. theorem OAI.SiegelZeros.WeightedTorusJets.W19.derivativeTriple_mem_next_rectangle line 298
  42. theorem OAI.SiegelZeros.WeightedTorusJets.W19.rectangularJetHom_generator_eq_zero line 307
  43. theorem OAI.SiegelZeros.WeightedTorusJets.W19.rectangle_span_le_jet_ker line 323
  44. def OAI.SiegelZeros.WeightedTorusJets.W19.rationalInvariant line 340
  45. theorem OAI.SiegelZeros.WeightedTorusJets.W19.rationalInvariant_commute line 344
  46. theorem OAI.SiegelZeros.WeightedTorusJets.W19.iter_rationalInvariant line 352
  47. theorem OAI.SiegelZeros.WeightedTorusJets.W19.derivativeTriple_rationalInvariant line 361