OAI/NumberTheory/Ostmann/QuadraticCenter/RightJacobiBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.QuadraticCenter.rightJacobi line 8
2. theorem OAI.Ostmann.QuadraticCenter.rightJacobi_mod line 10
3. theorem OAI.Ostmann.QuadraticCenter.rightJacobi_periodic line 19
4. theorem OAI.Ostmann.QuadraticCenter.rightJacobi_one line 23
5. theorem OAI.Ostmann.QuadraticCenter.rightJacobi_zero line 26
6. theorem OAI.Ostmann.QuadraticCenter.rightJacobi_mul line 29
7. theorem OAI.Ostmann.QuadraticCenter.rightJacobi_abs_le_one line 40