OAI/NumberTheory/PrimePackets/DiscriminantBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PrimeDegreePackets.integralBasis_discriminant_index line 128
  2. theorem OAI.PrimeDegreePackets.abs_discr_le_integral_basis line 162
  3. lemma OAI.PrimeDegreePackets.norm_det_le_factorial_pow line 177
  4. theorem OAI.PrimeDegreePackets.abs_discr_le_integral_basis_height line 199
  5. def OAI.PrimeDegreePackets.orderedEuclideanMap line 227
  6. lemma OAI.PrimeDegreePackets.integralEuclideanBasis_exists line 233
  7. lemma OAI.PrimeDegreePackets.integralEuclideanBasis_span line 278
  8. lemma OAI.PrimeDegreePackets.orderedEuclideanMap_integer_shortest line 291
  9. theorem OAI.PrimeDegreePackets.totallyReal_small_integral_basis line 313
  10. lemma OAI.PrimeDegreePackets.orderedUnitLogOnto_ker_unit_eq_one_or_neg_one line 363
  11. lemma OAI.PrimeDegreePackets.orderedUnitLogOnto_ker_card_totallyReal line 386
  12. theorem OAI.PrimeDegreePackets.lintegral_arithmeticFlowGaussian_units_totallyReal line 419
  13. theorem OAI.PrimeDegreePackets.lintegral_arithmeticFlowGaussian_ideal_totallyReal line 435
  14. theorem OAI.PrimeDegreePackets.fractionalIdealTheta_unit_unfolding_totallyReal line 469
  15. theorem OAI.PrimeDegreePackets.HeckeMellin.fractionalIdealTheta_mellin_lintegral_totallyReal line 489