OAI/NumberTheory/SiegelZeros/Structure/Radicand.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.W56.conductor_eight_of_signedConductor_twice_square line 15
2. theorem OAI.SiegelZeros.W56.reduced_radicand_ne_two line 30
3. theorem OAI.SiegelZeros.W56.characterField_squarefree_radicand_nonexceptional line 39
4. theorem OAI.SiegelZeros.Awei.W39.actual_squarefree_radicand_with_prime_signs line 59