OAI/NumberTheory/Jacobsthal/Partitions/SourceDenseCellContradiction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.ErdosInverseRefinement.cofactor_coprime_excluded_bin line 15
2. theorem OAI.Erdos970.ErdosInverseRefinement.cofactor_coprime_small line 35
3. theorem OAI.Erdos970.ErdosInverseRefinement.distinct_bins_coprime line 52
4. theorem OAI.Erdos970.ErdosInverseRefinement.parent_product_le_of_child_log line 69
5. theorem OAI.Erdos970.ErdosInverseRefinement.parent_small_coprime_child line 86
6. theorem OAI.Erdos970.ErdosInverseRefinement.source_no_dense_cell line 108