OAI/NumberTheory/JointDickman/Probability/QuotientSiteUnion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The divisor and quotient together cover the full prime site

  1. theorem OAI.JointDickman.coefficientPrimeSet_union_quotient line 10
  2. theorem OAI.JointDickman.coefficient_residue_base_product line 31
  3. theorem OAI.JointDickman.arithmetic_split_weight_le line 47