OAI/NumberTheory/Jacobsthal/Siegel/SumLogDivFilterDvdTwoMul.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.WeightedTorusJets.sum_log_div_filter_dvd_two_mul_le line 19
2. theorem OAI.Erdos970.WeightedTorusJets.source_good_prime_mass_with_chebyshev_constant line 34
3. theorem OAI.Erdos970.WeightedTorusJets.good_prime_filter_max_two line 76
4. theorem OAI.Erdos970.WeightedTorusJets.good_prime_mass_extend_small_parameters line 88
5. theorem OAI.Erdos970.WeightedTorusJets.source_good_prime_mass_all_parameters line 117
6. theorem OAI.Erdos970.WeightedTorusJets.primitive_eighth_root_difference_pow line 152
7. theorem OAI.Erdos970.WeightedTorusJets.cyclotomic_eight_sqrt_two_action line 178
8. theorem OAI.Erdos970.WeightedTorusJets.chiEight_not_factorsThrough_four line 190
9. theorem OAI.Erdos970.WeightedTorusJets.chiEight_isPrimitive line 201
10. theorem OAI.Erdos970.WeightedTorusJets.cyclotomic_eight_adjoin_eq_characterField line 221
11. theorem OAI.Erdos970.WeightedTorusJets.quadratic_character_eq_of_characterField_eq line 260
12. theorem OAI.Erdos970.WeightedTorusJets.primitive_level_eq_eight_of_same_lifted_characterField line 278
13. theorem OAI.Erdos970.WeightedTorusJets.primitive_level_eq_eight_of_sqrt_two_field line 299
14. theorem OAI.Erdos970.WeightedTorusJets.primitive_level_eq_eight_of_lifted_sqrt_two_field line 332