OAI/NumberTheory/Jacobsthal/Siegel/QuadraticAdjoinBasis.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.trace_norm_quadratic_basis line 20
  2. theorem OAI.Erdos970.WeightedTorusJets.rat_int_of_squarefree_mul_sq_eq_int line 46
  3. theorem OAI.Erdos970.WeightedTorusJets.integral_quadratic_half_coordinates line 65
  4. theorem OAI.Erdos970.WeightedTorusJets.even_coordinates_of_four_dvd line 88
  5. theorem OAI.Erdos970.WeightedTorusJets.even_sub_coordinates_of_four_dvd line 95
  6. theorem OAI.Erdos970.WeightedTorusJets.integral_quadratic_eq_int_add_int_mul line 102
  7. theorem OAI.Erdos970.WeightedTorusJets.integral_quadratic_eq_int_add_int_mul_half line 126
  8. theorem OAI.Erdos970.WeightedTorusJets.integral_quadratic_half_generator line 147
  9. theorem OAI.Erdos970.WeightedTorusJets.exists_ringOfIntegers_pair_basis line 160
  10. theorem OAI.Erdos970.WeightedTorusJets.discr_quadratic_pair line 188
  11. theorem OAI.Erdos970.WeightedTorusJets.coe_discr_eq_pair_of_integer_basis line 211
  12. theorem OAI.Erdos970.WeightedTorusJets.numberField_discr_quadratic_eq_four_mul line 223
  13. theorem OAI.Erdos970.WeightedTorusJets.numberField_discr_quadratic_eq_self line 237
  14. theorem OAI.Erdos970.WeightedTorusJets.isFundamentalDiscr_quadratic line 253
  15. theorem OAI.Erdos970.WeightedTorusJets.isUnramifiedIn_two_iff_radical_mod_four line 268
  16. theorem OAI.Erdos970.WeightedTorusJets.isUnramifiedIn_of_numberField_extension line 293
  17. theorem OAI.Erdos970.WeightedTorusJets.quadratic_radical_mod_four_of_odd_cyclotomic_overfield line 305
  18. def OAI.Erdos970.WeightedTorusJets.quadraticAdjoinBasis line 318
  19. theorem OAI.Erdos970.WeightedTorusJets.quadraticAdjoinBasis_apply line 326
  20. theorem OAI.Erdos970.WeightedTorusJets.primitive_odd_quadratic_signed_level_mod_four line 337
  21. def OAI.Erdos970.WeightedTorusJets.crtUnits line 395
  22. theorem OAI.Erdos970.WeightedTorusJets.crtUnits_fst line 400
  23. theorem OAI.Erdos970.WeightedTorusJets.crtUnits_snd line 408
  24. def OAI.Erdos970.WeightedTorusJets.crtCharacterLeft line 415
  25. def OAI.Erdos970.WeightedTorusJets.crtCharacterRight line 420
  26. theorem OAI.Erdos970.WeightedTorusJets.crtCharacterLeft_apply_unit line 426
  27. theorem OAI.Erdos970.WeightedTorusJets.crtCharacterRight_apply_unit line 432
  28. theorem OAI.Erdos970.WeightedTorusJets.crtCharacter_decomposition line 437
  29. theorem OAI.Erdos970.WeightedTorusJets.crtCharacterLeft_isPrimitive line 455
  30. theorem OAI.Erdos970.WeightedTorusJets.crtCharacterRight_isPrimitive line 469
  31. theorem OAI.Erdos970.WeightedTorusJets.changeLevel_neg_one line 484
  32. theorem OAI.Erdos970.WeightedTorusJets.crtCharacter_neg_one line 490