OAI/Combinatorics/Progressions/Linear/RationalSpanCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.span_submodule_basis line 14
  2. theorem OAI.Erdos3.real_span_rational_family line 19
  3. theorem OAI.Erdos3.realification_layer_eq_span line 25
  4. theorem OAI.Erdos3.exists_finite_layer_spanning line 39
  5. theorem OAI.Erdos3.rationalLieInclusion_integer_combination line 48
  6. theorem OAI.Erdos3.real_span_family_coordinates line 71
  7. theorem OAI.Erdos3.real_span_family_mem_iff_coordinates line 80
  8. theorem OAI.Erdos3.real_span_sum_family line 88
  9. theorem OAI.Erdos3.span_conditional_basis line 99