OAI/NumberTheory/Jacobsthal/Siegel/SqrtTwoField.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.primitive_mod_four_character_neg_one line 17
  2. theorem OAI.Erdos970.WeightedTorusJets.primitive_four_mul_exists_odd_part line 34
  3. theorem OAI.Erdos970.WeightedTorusJets.primitive_four_mul_quadratic_signed_part_mod_four line 45
  4. theorem OAI.Erdos970.WeightedTorusJets.fundamentalDiscr_eight_odd_case line 60
  5. theorem OAI.Erdos970.WeightedTorusJets.fundamentalDiscr_four_parity_case line 79
  6. theorem OAI.Erdos970.WeightedTorusJets.exists_signed_squarefree_characterField_generator line 103
  7. theorem OAI.Erdos970.WeightedTorusJets.normalized_signed_conductor_isFundamentalDiscr line 166
  8. theorem OAI.Erdos970.WeightedTorusJets.characterField_discr_eq_signed_conductor line 184
  9. theorem OAI.Erdos970.WeightedTorusJets.characterField_changeLevel_discr_eq_signed_conductor line 235
  10. theorem OAI.Erdos970.WeightedTorusJets.characterField_changeLevel_discr_natAbs line 251
  11. theorem OAI.Erdos970.WeightedTorusJets.quadraticAdjoin_discriminant line 268
  12. def OAI.Erdos970.WeightedTorusJets.sourceSqrtTwoField line 314
  13. theorem OAI.Erdos970.WeightedTorusJets.sourceSqrtTwoField_root_sq line 320
  14. theorem OAI.Erdos970.WeightedTorusJets.exists_auxiliary_sqrt_pair_of_field_ne line 334
  15. theorem OAI.Erdos970.WeightedTorusJets.source_biquadratic_arithmetic_of_field_ne line 394
  16. theorem OAI.Erdos970.WeightedTorusJets.source_biquadratic_arithmetic_canonical_of_field_ne line 476