OAI/NumberTheory/SiegelZeros/Structure/ConcreteArchimedean.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SiegelZeros.W10.rootField line 19
  2. theorem OAI.SiegelZeros.W10.leftRoot_mem line 25
  3. theorem OAI.SiegelZeros.W10.rightRoot_mem line 29
  4. def OAI.SiegelZeros.W10.adjoinGenerators line 32
  5. theorem OAI.SiegelZeros.W10.coe_adjoinGenerators line 41
  6. theorem OAI.SiegelZeros.W10.adjoinGenerators_linearIndependent line 45
  7. theorem OAI.SiegelZeros.W10.rootField_toSubalgebra line 56
  8. def OAI.SiegelZeros.W10.adjoinBasisOfCoordinates line 74
  9. theorem OAI.SiegelZeros.W10.adjoinBasisOfCoordinates_apply line 83
  10. theorem OAI.SiegelZeros.W10.rootField_finrank_of_coordinates line 91
  11. theorem OAI.SiegelZeros.W10.rootField_coordinates line 99
  12. def OAI.SiegelZeros.W10.rootFieldBasis line 117
  13. theorem OAI.SiegelZeros.W10.rootFieldBasis_apply line 123
  14. def OAI.SiegelZeros.W10.coordinateFieldEquiv line 129
  15. theorem OAI.SiegelZeros.W10.coordinateFieldEquiv_apply line 140
  16. def OAI.SiegelZeros.W10.squarefreeRootFieldBasis line 147
  17. theorem OAI.SiegelZeros.W10.squarefreeRootField_finrank line 153
  18. theorem OAI.SiegelZeros.W10.finiteRatModule_of_basis line 160
  19. theorem OAI.SiegelZeros.W10.squarefreeRootField_numberField line 166
  20. theorem OAI.SiegelZeros.W10.adjoinGenerators_isIntegral line 174
  21. theorem OAI.SiegelZeros.W10.squarefreeRootFieldBasis_isIntegral line 181
  22. def OAI.SiegelZeros.WeightedTorusJets.W11.signAlg line 194
  23. def OAI.SiegelZeros.WeightedTorusJets.W11.fieldSignAction line 202
  24. theorem OAI.SiegelZeros.WeightedTorusJets.W11.fieldSignAction_on_model line 210
  25. theorem OAI.SiegelZeros.WeightedTorusJets.W11.fieldSignAction_comp line 218
  26. theorem OAI.SiegelZeros.WeightedTorusJets.W11.fieldSignAction_injective line 228
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W11.fieldSigma_theta line 243
  28. def OAI.SiegelZeros.WeightedTorusJets.W11.squarefreeFieldSignAction line 252
  29. theorem OAI.SiegelZeros.WeightedTorusJets.W11.coordinateFieldEquiv_a line 260
  30. theorem OAI.SiegelZeros.WeightedTorusJets.W11.coordinateFieldEquiv_b line 268
  31. theorem OAI.SiegelZeros.WeightedTorusJets.W11.fieldSignAction_a line 276
  32. theorem OAI.SiegelZeros.WeightedTorusJets.W11.fieldSignAction_b line 285
  33. theorem OAI.SiegelZeros.WeightedTorusJets.W11.squarefreeFieldSignAction_a line 293
  34. theorem OAI.SiegelZeros.WeightedTorusJets.W11.squarefreeFieldSignAction_b line 302
  35. theorem OAI.SiegelZeros.WeightedTorusJets.W11.squarefreeSigma_a line 311
  36. theorem OAI.SiegelZeros.WeightedTorusJets.W11.squarefreeSigma_b line 317
  37. theorem OAI.SiegelZeros.WeightedTorusJets.W11.squarefreeTau_a line 323
  38. theorem OAI.SiegelZeros.WeightedTorusJets.W11.squarefreeTau_b line 329
  39. theorem OAI.SiegelZeros.WeightedTorusJets.W11.squarefreeSigmaTau_a line 335
  40. theorem OAI.SiegelZeros.WeightedTorusJets.W11.squarefreeSigmaTau_b line 341
  41. def OAI.SiegelZeros.SiegelZerosAwei.W36.rootA line 360
  42. def OAI.SiegelZeros.SiegelZerosAwei.W36.rootB line 362
  43. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.rootA_sq line 365
  44. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.rootB_sq line 371
  45. def OAI.SiegelZeros.SiegelZerosAwei.W36.concreteDirections line 376
  46. def OAI.SiegelZeros.SiegelZerosAwei.W36.concreteThetaMatrix line 386
  47. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.finrankRatModule_eq_four line 394
  48. theorem OAI.SiegelZeros.SiegelZerosAwei.W36.concrete_archimedean_norm_bound line 400