OAI/Combinatorics/Ryser/LineCover/SamplingNumerics.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.LineCover.half_pow_le_descFactorial line 12
2. theorem OAI.RyserCoveringCounterexample.LineCover.descFactorial_cast_pos line 26
3. theorem OAI.RyserCoveringCounterexample.LineCover.low_occupancy_quotient_le line 30
4. theorem OAI.RyserCoveringCounterexample.LineCover.high_occupancy_quotient_le line 50
5. theorem OAI.RyserCoveringCounterexample.LineCover.low_occupancy_exponent_neg line 73
6. theorem OAI.RyserCoveringCounterexample.LineCover.high_occupancy_exponent_neg line 80