OAI/NumberTheory/SiegelZeros/Structure/QuadraticEigencharacter.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SiegelZeros.WeightedTorusJets.exists_root_normalizing_automorphism line 15
2. lemma OAI.SiegelZeros.WeightedTorusJets.exists_embedding_principal_roots line 35
3. lemma OAI.SiegelZeros.WeightedTorusJets.basis_fieldRange_eq_adjoin line 55
4. lemma OAI.SiegelZeros.WeightedTorusJets.exists_principal_root_field_equiv line 81
5. lemma OAI.SiegelZeros.WeightedTorusJets.integral_autCongr_equivariant line 106
6. lemma OAI.SiegelZeros.WeightedTorusJets.integer_frobenius_transport line 113
7. lemma OAI.SiegelZeros.WeightedTorusJets.integer_two_direction_frobenius_transport line 123
8. lemma OAI.SiegelZeros.WeightedTorusJets.transported_sign_actions line 135
9. lemma OAI.SiegelZeros.WeightedTorusJets.transported_four_automorphisms line 143
10. theorem OAI.SiegelZeros.WeightedTorusJets.adjoin_simple_eq_of_sq_eq line 164
11. theorem OAI.SiegelZeros.WeightedTorusJets.adjoin_sqrt_two_map line 178
12. theorem OAI.SiegelZeros.WeightedTorusJets.sqrt_two_field_exclusion_map_iff line 188
13. theorem OAI.SiegelZeros.WeightedTorusJets.sourceSqrtTwoField_exclusion_map_iff line 199
14. theorem OAI.SiegelZeros.WeightedTorusJets.source_biquadratic_arithmetic_principal_of_field_ne line 213
15. theorem OAI.SiegelZeros.WeightedTorusJets.characterField_ne_sourceSqrtTwoField_of_ne_eight line 322
16. def OAI.SiegelZeros.WeightedTorusJets.quadraticEigencharacter line 345
17. lemma OAI.SiegelZeros.WeightedTorusJets.quadraticEigencharacter_apply_mul line 353
18. lemma OAI.SiegelZeros.WeightedTorusJets.quadraticEigencharacter_range line 358
19. lemma OAI.SiegelZeros.WeightedTorusJets.quadraticEigencharacter_eq_neg_one_iff line 364
20. theorem OAI.SiegelZeros.WeightedTorusJets.source_quadratic_group_character line 374