OAI/NumberTheory/Ostmann/Characters/FactorialContradictionHilbert.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.Characters.parity_permutation_comparisonline 13 - theorem
OAI.Ostmann.Characters.parity_family_impossibleline 26 - theorem
OAI.Ostmann.Characters.exists_depth_no_parity_familiesline 57