OAI/Combinatorics/Ryser/Field/SubfieldBound.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RyserCoveringCounterexample.subfield_card_lt_of_ne_top line 10
2. theorem OAI.RyserCoveringCounterexample.subfield_natCard_lt_of_ne_top line 21
3. theorem OAI.RyserCoveringCounterexample.subfield_card_eq_char_of_prime_degree line 29
4. theorem OAI.RyserCoveringCounterexample.subfield_natCard_eq_char_of_prime_degree line 50
5. theorem OAI.RyserCoveringCounterexample.subfield_card_cube_le_of_prime_degree line 58
6. theorem OAI.RyserCoveringCounterexample.subfield_natCard_cube_le_of_prime_degree line 65
7. theorem OAI.RyserCoveringCounterexample.subfield_eq_top_of_card_eq_char line 71