OAI/Combinatorics/Ryser/Field/Extension.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RyserCoveringCounterexample.ExtensionField line 7
2. instance OAI.RyserCoveringCounterexample.extensionFieldFintype line 9
3. theorem OAI.RyserCoveringCounterexample.extensionField_card line 12
4. theorem OAI.RyserCoveringCounterexample.extensionField_finrank line 16
5. def OAI.RyserCoveringCounterexample.primeEmbedding line 20
6. theorem OAI.RyserCoveringCounterexample.primeEmbedding_injective line 23
7. theorem OAI.RyserCoveringCounterexample.primeEmbedding_eq_iff line 27
8. def OAI.RyserCoveringCounterexample.extensionFieldDegreeOneEquiv line 31