OAI/NumberTheory/SiegelZeros/Structure/QuadraticAdjoinBasis.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.trace_norm_quadratic_basis line 18
  2. theorem OAI.SiegelZeros.WeightedTorusJets.rat_int_of_squarefree_mul_sq_eq_int line 44
  3. theorem OAI.SiegelZeros.WeightedTorusJets.integral_quadratic_half_coordinates line 63
  4. theorem OAI.SiegelZeros.WeightedTorusJets.even_coordinates_of_four_dvd line 86
  5. theorem OAI.SiegelZeros.WeightedTorusJets.even_sub_coordinates_of_four_dvd line 93
  6. theorem OAI.SiegelZeros.WeightedTorusJets.integral_quadratic_eq_int_add_int_mul line 100
  7. theorem OAI.SiegelZeros.WeightedTorusJets.integral_quadratic_eq_int_add_int_mul_half line 124
  8. theorem OAI.SiegelZeros.WeightedTorusJets.integral_quadratic_half_generator line 145
  9. theorem OAI.SiegelZeros.WeightedTorusJets.exists_ringOfIntegers_pair_basis line 158
  10. theorem OAI.SiegelZeros.WeightedTorusJets.discr_quadratic_pair line 186
  11. theorem OAI.SiegelZeros.WeightedTorusJets.coe_discr_eq_pair_of_integer_basis line 209
  12. theorem OAI.SiegelZeros.WeightedTorusJets.numberField_discr_quadratic_eq_four_mul line 221
  13. theorem OAI.SiegelZeros.WeightedTorusJets.numberField_discr_quadratic_eq_self line 235
  14. theorem OAI.SiegelZeros.WeightedTorusJets.isFundamentalDiscr_quadratic line 251
  15. theorem OAI.SiegelZeros.WeightedTorusJets.isUnramifiedIn_two_iff_radical_mod_four line 266
  16. theorem OAI.SiegelZeros.WeightedTorusJets.isUnramifiedIn_of_numberField_extension line 291
  17. theorem OAI.SiegelZeros.WeightedTorusJets.quadratic_radical_mod_four_of_odd_cyclotomic_overfield line 303
  18. def OAI.SiegelZeros.WeightedTorusJets.quadraticAdjoinBasis line 316
  19. theorem OAI.SiegelZeros.WeightedTorusJets.quadraticAdjoinBasis_apply line 324
  20. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_odd_quadratic_signed_level_mod_four line 335
  21. def OAI.SiegelZeros.WeightedTorusJets.crtUnits line 393
  22. theorem OAI.SiegelZeros.WeightedTorusJets.crtUnits_fst line 398
  23. theorem OAI.SiegelZeros.WeightedTorusJets.crtUnits_snd line 406
  24. def OAI.SiegelZeros.WeightedTorusJets.crtCharacterLeft line 413
  25. def OAI.SiegelZeros.WeightedTorusJets.crtCharacterRight line 418
  26. theorem OAI.SiegelZeros.WeightedTorusJets.crtCharacterLeft_apply_unit line 424
  27. theorem OAI.SiegelZeros.WeightedTorusJets.crtCharacterRight_apply_unit line 430
  28. theorem OAI.SiegelZeros.WeightedTorusJets.crtCharacter_decomposition line 435
  29. theorem OAI.SiegelZeros.WeightedTorusJets.crtCharacterLeft_isPrimitive line 453
  30. theorem OAI.SiegelZeros.WeightedTorusJets.crtCharacterRight_isPrimitive line 467
  31. theorem OAI.SiegelZeros.WeightedTorusJets.changeLevel_neg_one line 482
  32. theorem OAI.SiegelZeros.WeightedTorusJets.crtCharacter_neg_one line 488