OAI/NumberTheory/Jacobsthal/Sieve/IntegerRichLine.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosRichLine.integerComplexification line 12
2. theorem OAI.Erdos970.ErdosRichLine.integerComplexification_degree line 15
3. theorem OAI.Erdos970.ErdosRichLine.integerComplexification_eval line 20
4. theorem OAI.Erdos970.ErdosRichLine.integer_polynomial_rich_line line 30