OAI/NumberTheory/SiegelZeros/Characters/GaussSquarefreeBridge.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SiegelZeros.W56.exists_squarefree_int_factor line 13
2. theorem OAI.SiegelZeros.W56.squarefree_factor_natAbs_le line 30
3. theorem OAI.SiegelZeros.W56.normalized_root_sq line 38
4. theorem OAI.SiegelZeros.W56.adjoin_normalized_root_eq line 46
5. theorem OAI.SiegelZeros.W56.exists_squarefree_root_same_field line 67
6. theorem OAI.SiegelZeros.W56.root_radicand_ne_one line 86
7. theorem OAI.SiegelZeros.W56.characterField_squarefree_radicand line 102