OAI/Combinatorics/Progressions/Estimates/AllocatedExternalCandidatePreparedPhysicalConclusion.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CommonKeepPositiveKernelPreparation.conclusion_of_actualNativeQuotient line 68
2. def OAI.Erdos3.VectorPolynomial.PrimitiveFrontQuotientPhysicalTerminalAt line 166
3. theorem OAI.Erdos3.VectorPolynomial.exists_primitiveFrontQuotient_actual_physical_terminal line 245
4. def OAI.Erdos3.VectorPolynomial.PrimitiveFrontQuotientCanonicalPhysicalTerminalAt line 368
5. theorem OAI.Erdos3.VectorPolynomial.PrimitiveFrontQuotientPhysicalTerminalAt.toCanonical line 443
6. theorem OAI.Erdos3.VectorPolynomial.exists_primitiveFrontQuotient_canonical_physical_terminal line 560
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.PrimitiveFrontQuotientData.conclusion_of_canonicalPhysicalTerminal line 698