OAI/NumberTheory/SiegelZeros/Structure/SqrtTwoField.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_mod_four_character_neg_one line 15
  2. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_four_mul_exists_odd_part line 32
  3. theorem OAI.SiegelZeros.WeightedTorusJets.primitive_four_mul_quadratic_signed_part_mod_four line 43
  4. theorem OAI.SiegelZeros.WeightedTorusJets.fundamentalDiscr_eight_odd_case line 58
  5. theorem OAI.SiegelZeros.WeightedTorusJets.fundamentalDiscr_four_parity_case line 77
  6. theorem OAI.SiegelZeros.WeightedTorusJets.exists_signed_squarefree_characterField_generator line 101
  7. theorem OAI.SiegelZeros.WeightedTorusJets.normalized_signed_conductor_isFundamentalDiscr line 164
  8. theorem OAI.SiegelZeros.WeightedTorusJets.characterField_discr_eq_signed_conductor line 182
  9. theorem OAI.SiegelZeros.WeightedTorusJets.characterField_changeLevel_discr_eq_signed_conductor line 226
  10. theorem OAI.SiegelZeros.WeightedTorusJets.characterField_changeLevel_discr_natAbs line 242
  11. theorem OAI.SiegelZeros.WeightedTorusJets.quadraticAdjoin_discriminant line 259
  12. def OAI.SiegelZeros.WeightedTorusJets.sourceSqrtTwoField line 305
  13. theorem OAI.SiegelZeros.WeightedTorusJets.sourceSqrtTwoField_root_sq line 311
  14. theorem OAI.SiegelZeros.WeightedTorusJets.exists_auxiliary_sqrt_pair_of_field_ne line 325
  15. theorem OAI.SiegelZeros.WeightedTorusJets.source_biquadratic_arithmetic_of_field_ne line 385
  16. theorem OAI.SiegelZeros.WeightedTorusJets.source_biquadratic_arithmetic_canonical_of_field_ne line 467