OAI/NumberTheory/JointDickman/Arithmetic/BrunBlocks.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Products of even truncations over disjoint prime blocks

  1. def OAI.JointDickman.brunBlockChoices line 9
  2. def OAI.JointDickman.brunBlockUnion line 14
  3. def OAI.JointDickman.brunBlockSign line 17
  4. theorem OAI.JointDickman.brunBlockChoices_mem line 20
  5. theorem OAI.JointDickman.brunBlockSign_abs line 25
  6. theorem OAI.JointDickman.brunBlockUnion_inter line 28
  7. theorem OAI.JointDickman.brunBlockUnion_injOn line 43
  8. theorem OAI.JointDickman.brunBlock_upper line 51
  9. theorem OAI.JointDickman.brunBlock_expansion line 65
  10. theorem OAI.JointDickman.brunBlock_main line 80