OAI/Combinatorics/Progressions/Geometry/AllocatedExternalCandidateSpatialNativeAdaptedConclusion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.conclusion_of_actualSourceProblemOn line 70
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.conclusion_of_actualSourceOptionQuotient line 91
3. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.actualSourceProblemOn_withKeep line 182
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.actualSourceProblemOn_withKeep_optionJoint line 190
5. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.conclusion_of_actualSourceAdaptedOptionQuotient line 275