OAI/NumberTheory/OrdinaryCorrelations/HighTrace/ClosedLine.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.OrdinaryCorrelations.SignedTrace.ClosedLine line 11
  2. def OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.treeSteps line 25
  3. def OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.children line 28
  4. def OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.NoReturnIncidence line 31
  5. def OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.Good line 34
  6. def OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.Uncorrupted line 40
  7. def OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.departures line 44
  8. lemma OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.endpoints_ne line 46
  9. lemma OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.label_residue_eq line 55
  10. lemma OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.all_departures_eq_children line 63
  11. theorem OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.good_singleton_two_departures line 80
  12. theorem OAI.OrdinaryCorrelations.SignedTrace.ClosedLine.good_center_prime_mean line 111