OAI/NumberTheory/Ostmann/Tree/PartitionProducts.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous product fibers for an arbitrary partition of the leaves

  1. def OAI.Ostmann.partitionProduct line 13
  2. def OAI.Ostmann.partitionCoordinates line 17
  3. def OAI.Ostmann.partitionProductFiberEquiv line 22

    Source documentation

    Fixing all component totals is the product of the individual product fibers.

    noncomputable def partitionProductFiberEquiv {L C G : Type*}
    [Fintype L] [DecidableEq C] [CommGroup G]
    (component : L → C) (P : C → G) :
    {m : L → G // partitionProduct component m = P} ≃
      (∀ c : C, {v : ({i : L // component i = c} → G) // ∏ i, v i = P c}) where
…

    Mentions: OAI.Ostmann.partitionProduct

  4. theorem OAI.Ostmann.sum_card_partition line 47
  5. theorem OAI.Ostmann.card_partitionProductFiber line 53
  6. theorem OAI.Ostmann.card_partitionProduct_filter line 74