OAI/NumberTheory/Jacobsthal/Sieve/EndpointCofactorSplit.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.NumberTheoryLean.FullIsolatedCofactor.isolated_product line 17
2. theorem OAI.Erdos970.NumberTheoryLean.FullIsolatedCofactor.full_word_isolated_product line 25
3. theorem OAI.Erdos970.NumberTheoryLean.FullIsolatedCofactor.full_cofactor_alignment_word line 35
4. theorem OAI.Erdos970.NumberTheoryLean.EndpointCofactorSplit.endpoint_cofactor_split line 62
5. theorem OAI.Erdos970.NumberTheoryLean.EndpointCofactorSplit.endpoint_extra_factor_pos line 94