OAI/Combinatorics/Progressions/Estimates/AllocatedCandidateZeroRestrictedNativeCommonTerminal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalChart.hasCommonRefilteredOrbitFactors_axisPolynomial_of_zero_restriction line 35
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalLocalCandidate.hasCommonRefilteredOrbitFactors_freezeAxes_of_zero_restriction line 110
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.problem_nativeFactors_of_zero_restriction line 145
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.withKeep_nativeFactors_of_zero_restriction line 166
5. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AxisFreezing.historyStageData_of_zero_restricted_factors line 252
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_forward_terminal_of_zero_restricted_candidates line 397
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_early_forward_terminal_of_zero_restricted_candidates line 600
8. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_early_forward_terminal_of_zero_restricted_fast_generators line 790
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_early_forward_terminal_of_zero_restricted_native_common_factors line 997