OAI/NumberTheory/Ostmann/QuadraticCenter/PoissonPhase.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Ostmann.QuadraticCenter.stdAddChar_eq_weylPhaseline 8 - theorem
OAI.Ostmann.QuadraticCenter.weylPhase_eq_of_sub_intline 15 - theorem
OAI.Ostmann.QuadraticCenter.bezout_center_divisibilityline 20 - theorem
OAI.Ostmann.QuadraticCenter.stdAddChar_common_centerline 27 - theorem
OAI.Ostmann.QuadraticCenter.jacobi_bezout_inverseline 43 - theorem
OAI.Ostmann.QuadraticCenter.jacobi_mul_bezout_inverseline 57