OAI/Combinatorics/Progressions/Lattices/AllocatedAffinePhysicalBoundsSuccessor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.problem_physicalIntegerPoint line 44
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.withKeep_physicalIntegerPoint line 47
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.withKeep_original_dense line 54
4. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.conclusion_normalized line 71
5. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.conclusion_of_withKeep_normalized line 78
6. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.CertifiedThresholdAffineRefinement.canonical_cutoff_le_recursive line 88
7. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_affinePhysicalTerminal_nativeReset_degreeRule line 170
8. structure OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AffinePhysicalTerminalData.SuccessorInputs line 365
9. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AffinePhysicalTerminalData.SuccessorInputs.conclusion_of_reset line 426
10. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.AffinePhysicalTerminalData.successorInputsOfBounds line 517
11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_affinePhysicalTerminal_zeroRestricted_degreeRule line 690
12. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_normalized_affinePhysicalTerminal_zeroRestricted_degreeRule line 834
13. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateProblem.conclusion_of_affinePhysicalTerminal_bounds_degreeRule line 1019