OAI/NumberTheory/SiegelZeros/Structure/InvariantJetMonomial.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantJet_monomial line 38
  2. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangleJetIdeal_length_le line 88
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.sum_pi_one line 122
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.sum_pi_two line 129
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.sum_pi_three line 148
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_selected_sum line 175
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_one_selected_sum line 216
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.rectangularTaylorThree_two_selected_sum line 253
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_selected_taylor_ringHom line 293
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.factorial_smul_quotient_monomial line 342
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_source_taylor_ringHom line 355
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_source_taylor_quotient_ringHom line 375