OAI/Combinatorics/Progressions/Geometry/AllocatedExternalCandidateSpatialNativeOrdinaryTerminal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.ActualAdaptedPivotQuotientLongPhysicalTerminal line 92
2. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.ActualAdaptedPivotQuotientLongFactors.exists_affine_physical_terminal line 172
3. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedExternalCandidateSpatialNativeFamily_actual_physical_terminal line 356
4. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSpatialNativeFamily.ordinaryData_of_actualAdaptedPivotQuotientLongPhysicalTerminal line 694