OAI/NumberTheory/Ostmann/Characters/TreeLeafProducts.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Leaf-product fibers in a full binary tree

  1. def OAI.Ostmann.TreeLeafTuple line 12
  2. instance OAI.Ostmann.treeLeafTupleFintype line 16
  3. def OAI.Ostmann.treeLeafProduct line 21
  4. abbrev OAI.Ostmann.TreeLeafFiber line 25
  5. instance OAI.Ostmann.treeLeafFiberFintype line 28
  6. def OAI.Ostmann.treeLeafFiberZeroEquiv line 34
  7. def OAI.Ostmann.treeLeafFiberSuccEquiv line 42

    Source documentation

    Exposing the product in the left half leaves independent product fibers below it.

    def treeLeafFiberSuccEquiv {U : Type*} [CommGroup U] (n : ℕ) (P : U) :
    TreeLeafFiber U (n + 1) P ≃
      Σ m : U, TreeLeafFiber U n m × TreeLeafFiber U n (P / m) where
…

    Mentions: OAI.Ostmann.TreeLeafFiber

  8. theorem OAI.Ostmann.card_treeLeafTuple line 61
  9. theorem OAI.Ostmann.card_treeLeafFiber line 71
  10. theorem OAI.Ostmann.sum_treeLeafFiber_succ line 85
  11. theorem OAI.Ostmann.sum_treeLeafTuple_by_product line 95