OAI/NumberTheory/Jacobsthal/Siegel/BiquadraticBasis.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.finrank_sup_quadratic line 13
  2. theorem OAI.Erdos970.WeightedTorusJets.biquadratic_monomials_integral line 33
  3. theorem OAI.Erdos970.WeightedTorusJets.span_pair_sqrt line 42
  4. theorem OAI.Erdos970.WeightedTorusJets.span_biquadratic_monomials line 51
  5. def OAI.Erdos970.WeightedTorusJets.biquadraticBasis line 65
  6. theorem OAI.Erdos970.WeightedTorusJets.biquadraticBasis_apply line 76
  7. theorem OAI.Erdos970.WeightedTorusJets.finrank_adjoin_sqrt line 84
  8. theorem OAI.Erdos970.WeightedTorusJets.adjoin_pair_generators line 110
  9. theorem OAI.Erdos970.WeightedTorusJets.finrank_adjoin_pair_sqrt line 136
  10. def OAI.Erdos970.WeightedTorusJets.sqrtPairBasis line 145
  11. theorem OAI.Erdos970.WeightedTorusJets.coe_sqrtPairBasis_apply line 159
  12. def OAI.Erdos970.WeightedTorusJets.biquadraticLinearMap line 172
  13. lemma OAI.Erdos970.WeightedTorusJets.biquadraticLinearMap_basis line 175
  14. lemma OAI.Erdos970.WeightedTorusJets.biquadraticLinearMap_mul line 179
  15. def OAI.Erdos970.WeightedTorusJets.biquadraticSignEquiv line 214
  16. lemma OAI.Erdos970.WeightedTorusJets.biquadraticSignEquiv_basis line 240
  17. lemma OAI.Erdos970.WeightedTorusJets.biquadratic_algEquiv_ext line 249
  18. lemma OAI.Erdos970.WeightedTorusJets.quadratic_algEquiv_dichotomy line 259
  19. lemma OAI.Erdos970.WeightedTorusJets.biquadratic_automorphism_eq_sign line 265
  20. lemma OAI.Erdos970.WeightedTorusJets.biquadraticSignEquiv_injective line 287
  21. lemma OAI.Erdos970.WeightedTorusJets.biquadratic_card_automorphisms line 313
  22. lemma OAI.Erdos970.WeightedTorusJets.biquadratic_isGalois line 325
  23. lemma OAI.Erdos970.WeightedTorusJets.biquadraticSignEquiv_mul line 334
  24. lemma OAI.Erdos970.WeightedTorusJets.biquadratic_automorphisms_commute line 351
  25. lemma OAI.Erdos970.WeightedTorusJets.biquadraticSignEquiv_identity line 360
  26. lemma OAI.Erdos970.WeightedTorusJets.biquadratic_four_automorphisms line 370
  27. lemma OAI.Erdos970.WeightedTorusJets.sqrtPair_isGalois line 385
  28. lemma OAI.Erdos970.WeightedTorusJets.sqrtPair_four_automorphisms line 407
  29. theorem OAI.Erdos970.WeightedTorusJets.ringOfIntegers_map_dvd_iff line 451
  30. theorem OAI.Erdos970.WeightedTorusJets.frobenius_congruence_descends line 485