OAI/Combinatorics/Progressions/Estimates/AllocatedOrdinaryLongPhysicalTerminalConclusion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_early_forward_terminal_of_native_common_factors line 57
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.exists_native_common_affine_physical_terminal line 311
3. def OAI.Erdos3.NilpotentLieFiltration.NativeCommonTerminal line 498
4. theorem OAI.Erdos3.NilpotentLieFiltration.NativeCommonTerminal.of_history line 524
5. theorem OAI.Erdos3.NilpotentLieFiltration.NativeCommonTerminal.of_native_common_terminal line 554
6. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.NativeCommonPhysicalTerminal line 682
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.NativeCommonPhysicalTerminal.to_terminal line 715
8. abbrev OAI.Erdos3.VectorPolynomial.nativePhysicalTerminalAffineBudget line 740
9. abbrev OAI.Erdos3.VectorPolynomial.nativePhysicalTerminalWorkBudget line 744
10. abbrev OAI.Erdos3.VectorPolynomial.nativePhysicalTerminalFullBudget line 748
11. theorem OAI.Erdos3.VectorPolynomial.nativePhysicalTerminalBudgets_nonneg line 754
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.NativeCommonPhysicalTerminal.exists_physicalData line 808
13. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.OrdinaryLongPhysicalTerminalData line 881
14. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_nativeCommonPhysicalTerminal_degreeRule line 985
15. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.OrdinaryLongPhysicalTerminalData.conclusion_of_bounds line 1123