OAI/NumberTheory/SiegelZeros/Characters/BiquadraticArithmeticFull.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.source_biquadratic_arithmetic_full line 22
  2. theorem OAI.SiegelZeros.WeightedTorusJets.source_biquadratic_arithmetic_canonical_full line 103
  3. theorem OAI.SiegelZeros.WeightedTorusJets.exists_lower_triangular_replacement line 146
  4. theorem OAI.SiegelZeros.WeightedTorusJets.determinant_dvd_of_earlier_row_replacement line 173
  5. theorem OAI.SiegelZeros.WeightedTorusJets.replacement_row_expansion line 196
  6. theorem OAI.SiegelZeros.WeightedTorusJets.replacement_row_sub_mem line 212
  7. theorem OAI.SiegelZeros.WeightedTorusJets.weighted_interpolation_determinant_dvd line 233
  8. theorem OAI.SiegelZeros.WeightedTorusJets.weighted_interpolation_determinant_dvd_of_frobenius_choice line 267
  9. theorem OAI.SiegelZeros.WeightedTorusJets.galois_derivative_determinant_mem_prime_power line 291
  10. theorem OAI.SiegelZeros.WeightedTorusJets.integral_jet_matrix_lift line 326
  11. theorem OAI.SiegelZeros.WeightedTorusJets.exists_integral_jet_determinant_divisible line 367
  12. theorem OAI.SiegelZeros.WeightedTorusJets.frobenius_action_choice_iff_mapRingHom line 412
  13. theorem OAI.SiegelZeros.WeightedTorusJets.frobenius_action_choice_quotient line 422