OAI/NumberTheory/SiegelZeros/Structure/MultiplicityCycles.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.W17.ConeLocalLength.mapped_minimalPrime_of_prime_extension line 26
  2. theorem OAI.SiegelZeros.W17.ConeLocalLength.minimalPrime_isHomogeneous line 36
  3. theorem OAI.SiegelZeros.W17.ConeLocalLength.conePrime_minimal_over_homogenized line 56
  4. theorem OAI.SiegelZeros.W17.ConeLocalLength.homogenized_span_isHomogeneous line 89
  5. theorem OAI.SiegelZeros.W17.ConeLocalLength.conePrime_isHomogeneous_of_minimal line 97
  6. theorem OAI.SiegelZeros.W17.ConeLocalLength.laurentPrime_height_eq line 107
  7. theorem OAI.SiegelZeros.W17.ConeLocalLength.conePrime_height_eq line 120
  8. def OAI.SiegelZeros.WeightedTorusJets.W22.RetainedMinimalPrime line 148
  9. instance OAI.SiegelZeros.WeightedTorusJets.W22.RetainedMinimalPrime.finiteFamily line 155
  10. instance OAI.SiegelZeros.WeightedTorusJets.W22.RetainedMinimalPrime.(instance at line 162) line 162
  11. def OAI.SiegelZeros.WeightedTorusJets.W22.RetainedMinimalPrime.toComponent line 164
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedMinimalPrime.toComponent_val line 173
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedMinimalPrime.toComponent_injective line 179
  14. def OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.canonicalRetainedCut line 190
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.canonicalRetainedCut_covers line 219
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.canonicalRetainedCut_next_le_target line 233
  17. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.retainedChild_dimension line 260
  18. def OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.equidimensionalRetainedCut line 283
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W22.RetainedPrimeCycle.equidimensionalRetainedCut_covers line 293
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W22.minimal_cut_of_intermediate_parent line 315
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W22.cut_ideal_homogeneous line 327
  22. theorem OAI.SiegelZeros.WeightedTorusJets.W22.natural_local_onecut_recurrence line 334
  23. def OAI.SiegelZeros.WeightedTorusJets.W22.parentChildIncidenceEquiv line 367
  24. def OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicityCycle line 391
  25. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicityCycle_coefficient line 401
  26. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicityCycle_cut_expansion line 419
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicityCycle_parent_budget line 471
  28. theorem OAI.SiegelZeros.WeightedTorusJets.W22.actualMultiplicityCycle_cut_degree_le line 514