OAI/NumberTheory/Ostmann/Quadratic/QuadraticBilinearTwist.lean
3 declarations, 0 contain sorry, 0 declared as axioms
The actual signed frequencies in the full correction matrices
- theorem
OAI.Ostmann.quadratic_gauss_bilinear_twistline 13 - theorem
OAI.Ostmann.quadratic_bilinear_twistline 31 - theorem
OAI.Ostmann.quadratic_sqrt_twist_commuteline 48