OAI/Combinatorics/SquareDifference/CRTTransfer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SquareDifference.combined_residue line 23
2. lemma OAI.SquareDifference.combined_modulus_coprime line 59
3. lemma OAI.SquareDifference.exists_combined_units line 73
4. def OAI.SquareDifference.smallResidueInput line 82
5. lemma OAI.SquareDifference.smallResidueInput_bound line 85
6. lemma OAI.SquareDifference.smallResidueInput_average line 94
7. lemma OAI.SquareDifference.smallResidue_fiber_identity line 108
8. lemma OAI.SquareDifference.actual_set_fiber_transfer line 120