OAI/NumberTheory/Jacobsthal/Harmonic/PolynomialLocalGraph.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos970.ErdosDivisibleInflection.planeEval line 16
2. theorem OAI.Erdos970.ErdosDivisibleInflection.contDiff_planeEval line 18
3. theorem OAI.Erdos970.ErdosDivisibleInflection.fderiv_planeEval_inr line 29
4. theorem OAI.Erdos970.ErdosDivisibleInflection.scalar_map_invertible line 42
5. def OAI.Erdos970.ErdosLocalFiberGraphs.boundedFiber line 62
6. def OAI.Erdos970.ErdosLocalFiberGraphs.verticalPolynomial line 65
7. theorem OAI.Erdos970.ErdosLocalFiberGraphs.verticalPolynomial_eval line 68
8. theorem OAI.Erdos970.ErdosLocalFiberGraphs.boundedFiber_finite line 77
9. theorem OAI.Erdos970.ErdosLocalFiberGraphs.boundedFiber_interior line 88
10. theorem OAI.Erdos970.ErdosLocalFiberGraphs.compact_nonzero_eventually line 96
11. theorem OAI.Erdos970.ErdosDivisibleInflection.exists_local_real_graph line 122