OAI/NumberTheory/JointDickman/Probability/ResidueProductError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Passing residue square errors through the two-endpoint product

  1. theorem OAI.JointDickman.restricted_residue_product_error line 10
  2. theorem OAI.JointDickman.restricted_residue_product_error_bound line 35