OAI/NumberTheory/Jacobsthal/Siegel/BiquadraticArithmeticFull.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.WeightedTorusJets.source_biquadratic_arithmetic_full line 35
2. theorem OAI.Erdos970.WeightedTorusJets.source_biquadratic_arithmetic_canonical_full line 116
3. theorem OAI.Erdos970.WeightedTorusJets.exists_lower_triangular_replacement line 168
4. theorem OAI.Erdos970.WeightedTorusJets.determinant_dvd_of_earlier_row_replacement line 195
5. theorem OAI.Erdos970.WeightedTorusJets.replacement_row_expansion line 218
6. theorem OAI.Erdos970.WeightedTorusJets.replacement_row_sub_mem line 234
7. theorem OAI.Erdos970.WeightedTorusJets.weighted_interpolation_determinant_dvd line 255
8. theorem OAI.Erdos970.WeightedTorusJets.weighted_interpolation_determinant_dvd_of_frobenius_choice line 289
9. theorem OAI.Erdos970.WeightedTorusJets.galois_derivative_determinant_mem_prime_power line 313
10. theorem OAI.Erdos970.WeightedTorusJets.integral_jet_matrix_lift line 348
11. theorem OAI.Erdos970.WeightedTorusJets.exists_integral_jet_determinant_divisible line 389
12. theorem OAI.Erdos970.WeightedTorusJets.frobenius_action_choice_iff_mapRingHom line 434
13. theorem OAI.Erdos970.WeightedTorusJets.frobenius_action_choice_quotient line 444