OAI/Combinatorics/BalancedRyser/Incidence/AffineDoubleCount.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Balanced.sum_line_count_eq_sum_point_count line 17
  2. theorem OAI.Balanced.sum_line_count line 24
  3. theorem OAI.Balanced.sum_sq_line_count_eq_sum_pair_count line 34
  4. theorem OAI.Balanced.sum_sq_line_count line 58
  5. theorem OAI.Balanced.common_line_count_of_existsUnique line 91
  6. theorem OAI.Balanced.sum_sq_line_count_of_unique line 102
  7. theorem OAI.Balanced.sum_line_count_real line 112
  8. theorem OAI.Balanced.sum_sq_line_count_real line 119