OAI/NumberTheory/SiegelZeros/Structure/FieldAutomorphisms.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SiegelZeros.WeightedTorusJets.W11.Biquad line 18
  2. def OAI.SiegelZeros.WeightedTorusJets.W11.flip line 21
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W11.flip_re line 30
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W11.flip_im line 33
  5. def OAI.SiegelZeros.WeightedTorusJets.W11.sigma line 36
  6. def OAI.SiegelZeros.WeightedTorusJets.W11.tau line 44
  7. def OAI.SiegelZeros.WeightedTorusJets.W11.a line 47
  8. def OAI.SiegelZeros.WeightedTorusJets.W11.b line 48
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W11.sigma_a line 50
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W11.sigma_b line 52
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W11.tau_a line 54
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W11.tau_b line 56
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W11.sigma_sigma line 59
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W11.tau_tau line 61
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W11.sigma_tau_commute line 63
  16. def OAI.SiegelZeros.WeightedTorusJets.W11.sigmaTau line 67
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W11.sigmaTau_apply line 69
  18. theorem OAI.SiegelZeros.WeightedTorusJets.W11.sigmaTau_sigmaTau line 71
  19. def OAI.SiegelZeros.WeightedTorusJets.W11.signAction line 76
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W11.signAction_comp line 80
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W11.signAction_injective line 86
  22. def OAI.SiegelZeros.WeightedTorusJets.W11.theta line 94
  23. theorem OAI.SiegelZeros.WeightedTorusJets.W11.sigma_theta line 97
  24. theorem OAI.SiegelZeros.WeightedTorusJets.W11.tau_theta line 100
  25. theorem OAI.SiegelZeros.WeightedTorusJets.W11.sigmaTau_theta line 103
  26. theorem OAI.SiegelZeros.WeightedTorusJets.W11.theta_injective line 107
  27. def OAI.SiegelZeros.WeightedTorusJets.W11.evalQuadratic line 116
  28. def OAI.SiegelZeros.WeightedTorusJets.W11.evalBiquad line 127
  29. theorem OAI.SiegelZeros.WeightedTorusJets.W11.evalBiquad_theta line 134
  30. theorem OAI.SiegelZeros.WeightedTorusJets.W11.evalBiquad_injective line 144
  31. theorem OAI.SiegelZeros.W10.square_root_not_rational line 175
  32. theorem OAI.SiegelZeros.W10.quadratic_coefficients_eq_zero line 183
  33. theorem OAI.SiegelZeros.W10.second_root_not_linear line 196
  34. theorem OAI.SiegelZeros.W10.quadratic_norm_eq_zero line 219
  35. theorem OAI.SiegelZeros.W10.biquadratic_coefficients_eq_zero line 233
  36. theorem OAI.SiegelZeros.W10.generators_linearIndependent_of_squares line 256
  37. theorem OAI.SiegelZeros.W10.rational_sq_ne_two line 273
  38. theorem OAI.SiegelZeros.W10.generators_linearIndependent_sqrt_two line 279
  39. theorem OAI.SiegelZeros.W10.rational_sq_ne_of_negative line 288
  40. theorem OAI.SiegelZeros.W10.generators_linearIndependent_of_negative_radicand line 293
  41. def OAI.SiegelZeros.WeightedTorusJets.W11.evalAlg line 308
  42. theorem OAI.SiegelZeros.WeightedTorusJets.W11.evalAlg_a line 316
  43. theorem OAI.SiegelZeros.WeightedTorusJets.W11.evalAlg_b line 321
  44. theorem OAI.SiegelZeros.WeightedTorusJets.W11.evalAlg_mem_adjoin line 327
  45. theorem OAI.SiegelZeros.WeightedTorusJets.W11.evalAlg_range line 338
  46. def OAI.SiegelZeros.WeightedTorusJets.W11.adjoinEquiv line 352
  47. theorem OAI.SiegelZeros.WeightedTorusJets.W11.adjoinEquiv_apply line 360
  48. def OAI.SiegelZeros.WeightedTorusJets.W11.sigmaAlg line 365
  49. def OAI.SiegelZeros.WeightedTorusJets.W11.tauAlg line 371
  50. def OAI.SiegelZeros.WeightedTorusJets.W11.adjoinSigma line 377
  51. def OAI.SiegelZeros.WeightedTorusJets.W11.adjoinTau line 384
  52. theorem OAI.SiegelZeros.WeightedTorusJets.W11.adjoinSigma_on_model line 391
  53. theorem OAI.SiegelZeros.WeightedTorusJets.W11.adjoinTau_on_model line 398
  54. theorem OAI.SiegelZeros.WeightedTorusJets.W11.adjoinSigma_a line 405
  55. theorem OAI.SiegelZeros.WeightedTorusJets.W11.adjoinSigma_b line 414
  56. theorem OAI.SiegelZeros.WeightedTorusJets.W11.adjoinSigma_involutive line 423
  57. theorem OAI.SiegelZeros.WeightedTorusJets.W11.adjoinTau_involutive line 431
  58. theorem OAI.SiegelZeros.WeightedTorusJets.W11.adjoinSigma_adjoinTau_commute line 439
  59. def OAI.SiegelZeros.WeightedTorusJets.W11.adjoinEquivOfNonsquares line 448