OAI/Combinatorics/Progressions/Linear/RationalTagConstraintBasis.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.realRationalCoordinateSpan_iInf line 14
2. theorem OAI.Erdos3.realRationalCoordinateSpan_top line 22
3. theorem OAI.Erdos3.realRationalCoordinateSpan_iInf_basis line 28
4. def OAI.Erdos3.VectorPolynomial.rationalTagConstraintIntersection line 51
5. theorem OAI.Erdos3.VectorPolynomial.exists_rationalTagConstraintList_basis line 55
6. theorem OAI.Erdos3.VectorPolynomial.constraint_realSpaces_member_iff line 71
7. theorem OAI.Erdos3.VectorPolynomial.rationalTagConstraintList_basis_member_iff line 87
8. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.exists_bounded_tag_bases line 110
9. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.exists_bounded_tag_bases_univ line 132