OAI/NumberTheory/SiegelZeros/Characters/BiquadraticBasis.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.finrank_sup_quadratic line 13
  2. theorem OAI.SiegelZeros.WeightedTorusJets.biquadratic_monomials_integral line 33
  3. theorem OAI.SiegelZeros.WeightedTorusJets.span_pair_sqrt line 42
  4. theorem OAI.SiegelZeros.WeightedTorusJets.span_biquadratic_monomials line 51
  5. def OAI.SiegelZeros.WeightedTorusJets.biquadraticBasis line 65
  6. theorem OAI.SiegelZeros.WeightedTorusJets.biquadraticBasis_apply line 76
  7. theorem OAI.SiegelZeros.WeightedTorusJets.finrank_adjoin_sqrt line 84
  8. theorem OAI.SiegelZeros.WeightedTorusJets.adjoin_pair_generators line 110
  9. theorem OAI.SiegelZeros.WeightedTorusJets.finrank_adjoin_pair_sqrt line 136
  10. def OAI.SiegelZeros.WeightedTorusJets.sqrtPairBasis line 145
  11. theorem OAI.SiegelZeros.WeightedTorusJets.coe_sqrtPairBasis_apply line 159
  12. def OAI.SiegelZeros.WeightedTorusJets.biquadraticLinearMap line 170
  13. lemma OAI.SiegelZeros.WeightedTorusJets.biquadraticLinearMap_basis line 173
  14. lemma OAI.SiegelZeros.WeightedTorusJets.biquadraticLinearMap_mul line 177
  15. def OAI.SiegelZeros.WeightedTorusJets.biquadraticSignEquiv line 212
  16. lemma OAI.SiegelZeros.WeightedTorusJets.biquadraticSignEquiv_basis line 238
  17. lemma OAI.SiegelZeros.WeightedTorusJets.biquadratic_algEquiv_ext line 247
  18. lemma OAI.SiegelZeros.WeightedTorusJets.quadratic_algEquiv_dichotomy line 257
  19. lemma OAI.SiegelZeros.WeightedTorusJets.biquadratic_automorphism_eq_sign line 263
  20. lemma OAI.SiegelZeros.WeightedTorusJets.biquadraticSignEquiv_injective line 285
  21. lemma OAI.SiegelZeros.WeightedTorusJets.biquadratic_card_automorphisms line 311
  22. lemma OAI.SiegelZeros.WeightedTorusJets.biquadratic_isGalois line 323
  23. lemma OAI.SiegelZeros.WeightedTorusJets.biquadraticSignEquiv_mul line 332
  24. lemma OAI.SiegelZeros.WeightedTorusJets.biquadratic_automorphisms_commute line 349
  25. lemma OAI.SiegelZeros.WeightedTorusJets.biquadraticSignEquiv_identity line 358
  26. lemma OAI.SiegelZeros.WeightedTorusJets.biquadratic_four_automorphisms line 368
  27. lemma OAI.SiegelZeros.WeightedTorusJets.sqrtPair_isGalois line 382
  28. lemma OAI.SiegelZeros.WeightedTorusJets.sqrtPair_four_automorphisms line 404
  29. theorem OAI.SiegelZeros.WeightedTorusJets.ringOfIntegers_map_dvd_iff line 448
  30. theorem OAI.SiegelZeros.WeightedTorusJets.frobenius_congruence_descends line 482