OAI/NumberTheory/PiExponent/LocalAlgebra/RetainedIntersectionCycles.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PiExponentJets.W22.ProjectiveComponent line 14
  2. instance OAI.PiExponentJets.W22.ProjectiveComponent.(instance at line 23) line 23
  3. theorem OAI.PiExponentJets.W22.ProjectiveComponent.homogeneous line 25
  4. def OAI.PiExponentJets.W22.ProjectiveComponent.coordinate line 28
  5. theorem OAI.PiExponentJets.W22.ProjectiveComponent.coordinate_not_mem line 31
  6. def OAI.PiExponentJets.W22.ProjectiveComponent.hilbertDegree line 36
  7. theorem OAI.PiExponentJets.W22.ProjectiveComponent.hilbertDegree_ge_one line 39
  8. structure OAI.PiExponentJets.W22.RetainedPrimeCycle line 47
  9. instance OAI.PiExponentJets.W22.RetainedPrimeCycle.(instance at line 57) line 57
  10. def OAI.PiExponentJets.W22.RetainedPrimeCycle.degree line 59
  11. def OAI.PiExponentJets.W22.RetainedPrimeCycle.coefficientAt line 62
  12. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.degree_nonneg line 66
  13. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.coefficientAt_le_degree line 72
  14. structure OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut line 87
  15. instance OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut.(instance at line 109) line 109
  16. def OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut.cutLength line 111
  17. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut.cutLength_spec line 114
  18. def OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut.next line 124
  19. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut.next_component line 130
  20. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut.next_coefficient line 133
  21. def OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut.CoversBelow line 136
  22. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut.parent_budget line 140
  23. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCut.degree_next_le line 154
  24. inductive OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCutHistory line 175
  25. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCutHistory.degree_bound line 182
  26. theorem OAI.PiExponentJets.W22.RetainedPrimeCycle.ProperCutHistory.coefficient_bound line 196