OAI/Combinatorics/Progressions/Lattices/CertifiedFullChartAffineTerminal.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.retainedTagProjection line 13
  2. theorem OAI.Erdos3.VectorPolynomial.retainedTagProjection_mem line 19
  3. theorem OAI.Erdos3.VectorPolynomial.retainedTagProjection_eq line 23
  4. theorem OAI.Erdos3.VectorPolynomial.retainedTagProjection_entry_le_one line 30
  5. def OAI.Erdos3.VectorPolynomial.fullTaggedLinearMapChart line 42
  6. def OAI.Erdos3.VectorPolynomial.fullTaggedAffineMapChart line 49
  7. theorem OAI.Erdos3.VectorPolynomial.fullTaggedLinearMapChart_homogeneous line 56
  8. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineMapChart_support line 68
  9. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineMapChart_top line 82
  10. theorem OAI.Erdos3.VectorPolynomial.fullTaggedLinearMapChart_eval_tag line 96
  11. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineMapChart_eval_tag line 113
  12. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineMapChart_top_mem_set line 122
  13. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineMapChart_eval_eq line 136
  14. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineMapChart_eval_eq_of_quotient line 149
  15. def OAI.Erdos3.VectorPolynomial.fullTaggedLinearRetraction line 161
  16. def OAI.Erdos3.VectorPolynomial.fullTaggedAffineRetraction line 168
  17. theorem OAI.Erdos3.VectorPolynomial.fullTaggedLinearRetraction_homogeneous line 176
  18. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineRetraction_support line 189
  19. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineRetraction_top line 204
  20. theorem OAI.Erdos3.VectorPolynomial.fullTaggedLinearRetraction_eval_tag line 218
  21. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineRetraction_eval_tag line 236
  22. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineRetraction_top_mem line 245
  23. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineRetraction_top_mem_set line 254
  24. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineRetraction_eval_eq line 264
  25. theorem OAI.Erdos3.VectorPolynomial.fullTaggedAffineRetraction_eval_eq_of_quotient line 276
  26. theorem OAI.Erdos3.VectorPolynomial.RationalTaggedConstraintCertificate.exists_affineRetraction line 287
  27. theorem OAI.Erdos3.NilpotentLieFiltration.CertifiedFullChartFiniteHistory.exists_affine_globalMarkedNativeFactors line 335
  28. theorem OAI.Erdos3.NilpotentLieFiltration.GlobalMarkedNativeFactors.affine_product_values line 384