OAI/NumberTheory/Ostmann/QuadraticCenter/DistinctGenerating.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.QuadraticCenter.distinctGeneratingline 9 - theorem
OAI.Ostmann.QuadraticCenter.distinctGenerating_eq_powersetline 12 - theorem
OAI.Ostmann.QuadraticCenter.distinctGenerating_coeffline 20 - theorem
OAI.Ostmann.QuadraticCenter.distinctGenerating_sign_countsline 31 - theorem
OAI.Ostmann.QuadraticCenter.sign_count_pairingline 56 - theorem
OAI.Ostmann.QuadraticCenter.even_generating_expansionline 67 - theorem
OAI.Ostmann.QuadraticCenter.paired_generating_coeffline 79