OAI/Combinatorics/Ryser/Incidence/PopularScalars.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.RyserCoveringCounterexample.Incidence.card_field_smul line 16
  2. theorem OAI.RyserCoveringCounterexample.Incidence.field_smul_smul line 23
  3. theorem OAI.RyserCoveringCounterexample.Incidence.field_one_smul line 32
  4. theorem OAI.RyserCoveringCounterexample.Incidence.field_smul_sub line 36
  5. theorem OAI.RyserCoveringCounterexample.Incidence.field_smul_inter line 55
  6. theorem OAI.RyserCoveringCounterexample.Incidence.quotient_overlap_card line 63
  7. theorem OAI.RyserCoveringCounterexample.Incidence.popular_difference_bound line 73
  8. theorem OAI.RyserCoveringCounterexample.Incidence.exists_popular_scalars line 109