OAI/NumberTheory/Ostmann/Construction/CanonicalOccurrenceTransportScalarTreeBasic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.rootCode line 10
  2. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.Plan.rootFrequency line 14
  3. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.Plan.leftPlan line 18
  4. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.Plan.rightPlan line 21
  5. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.rootCode_treeCode line 24
  6. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.treeRoot_plus_eq_of_code line 27
  7. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.plan_rootFrequency line 34