OAI/NumberTheory/SiegelZeros/Characters/SquarefreeRadicands.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.W10.squarefree_int_eq_one_of_rational_square line 13
2. theorem OAI.SiegelZeros.W10.squarefree_int_eq_two_of_twice_rational_square line 22
3. theorem OAI.SiegelZeros.W10.rational_sq_ne_squarefree_int line 43
4. theorem OAI.SiegelZeros.W10.rational_sq_ne_twice_squarefree_int line 48
5. theorem OAI.SiegelZeros.W10.generators_linearIndependent_squarefree line 53