OAI/NumberTheory/Jacobsthal/Partitions/EffectiveCoordinates.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosVarianceEffective.effectiveModulus line 13
2. def OAI.Erdos970.ErdosVarianceEffective.effectiveIntercept line 16
3. theorem OAI.Erdos970.ErdosVarianceEffective.effectiveModulus_pos line 19
4. theorem OAI.Erdos970.ErdosVarianceEffective.effectiveIntercept_identity line 22
5. theorem OAI.Erdos970.ErdosVarianceEffective.hitNumerator_coprime_effectiveModulus line 27
6. theorem OAI.Erdos970.ErdosVarianceEffective.effectiveIntercept_coprime line 31
7. theorem OAI.Erdos970.ErdosVarianceEffective.effective_coordinates_gcd line 40
8. theorem OAI.Erdos970.ErdosVarianceEffective.zero_effectiveIntercept_modulus_one line 44
9. theorem OAI.Erdos970.ErdosVarianceEffective.alignedCofactor_coprime_effectiveModulus line 49
10. theorem OAI.Erdos970.ErdosVarianceEffective.denominator_full_cofactor line 53