OAI/Combinatorics/Ryser/Incidence/ScalarCollisions.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.Incidence.card_collisionPairs_eq_sum_sq line 18
2. theorem OAI.RyserCoveringCounterexample.Incidence.card_sq_le_card_image_mul_collisionPairs line 47
3. theorem OAI.RyserCoveringCounterexample.Incidence.image_scalar_add line 63
4. theorem OAI.RyserCoveringCounterexample.Incidence.dilateSum_eq_add_smul line 74
5. theorem OAI.RyserCoveringCounterexample.Incidence.card_dilateSum_mul_scalarCollisionCount line 77
6. theorem OAI.RyserCoveringCounterexample.Incidence.card_field_lt_twice_of_dilateSum_card_le_real line 88
7. theorem OAI.RyserCoveringCounterexample.Incidence.card_field_lt_twice_of_dilateSum_card_le line 125