OAI/NumberTheory/Jacobsthal/Siegel/QuadraticEigencharacter.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Erdos970.WeightedTorusJets.exists_root_normalizing_automorphism line 17
2. lemma OAI.Erdos970.WeightedTorusJets.exists_embedding_principal_roots line 37
3. lemma OAI.Erdos970.WeightedTorusJets.basis_fieldRange_eq_adjoin line 57
4. lemma OAI.Erdos970.WeightedTorusJets.exists_principal_root_field_equiv line 83
5. lemma OAI.Erdos970.WeightedTorusJets.integral_autCongr_equivariant line 108
6. lemma OAI.Erdos970.WeightedTorusJets.integer_frobenius_transport line 115
7. lemma OAI.Erdos970.WeightedTorusJets.integer_two_direction_frobenius_transport line 125
8. lemma OAI.Erdos970.WeightedTorusJets.transported_sign_actions line 137
9. lemma OAI.Erdos970.WeightedTorusJets.transported_four_automorphisms line 145
10. theorem OAI.Erdos970.WeightedTorusJets.adjoin_simple_eq_of_sq_eq line 166
11. theorem OAI.Erdos970.WeightedTorusJets.adjoin_sqrt_two_map line 180
12. theorem OAI.Erdos970.WeightedTorusJets.sqrt_two_field_exclusion_map_iff line 190
13. theorem OAI.Erdos970.WeightedTorusJets.sourceSqrtTwoField_exclusion_map_iff line 201
14. theorem OAI.Erdos970.WeightedTorusJets.source_biquadratic_arithmetic_principal_of_field_ne line 215
15. theorem OAI.Erdos970.WeightedTorusJets.characterField_ne_sourceSqrtTwoField_of_ne_eight line 324
16. def OAI.Erdos970.WeightedTorusJets.quadraticEigencharacter line 347
17. lemma OAI.Erdos970.WeightedTorusJets.quadraticEigencharacter_apply_mul line 355
18. lemma OAI.Erdos970.WeightedTorusJets.quadraticEigencharacter_range line 360
19. lemma OAI.Erdos970.WeightedTorusJets.quadraticEigencharacter_eq_neg_one_iff line 366
20. theorem OAI.Erdos970.WeightedTorusJets.source_quadratic_group_character line 376