BinomialBiproduct.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExternalTensor.Binomial.biproductBiprod line 14
Source documentation
Distribute a finite biproduct of binary biproducts and retain the two branch labels.
```
def biproductBiprod {I : Type} [Fintype I] (f g : I → C) :
    (⨁ fun i => f i ⊞ g i) ≅ ⨁ (Sum.elim f g) where
…
```

def OAI.ExternalTensor.Binomial.splitShift line 43

Source documentation

Shift a binary splitting, using the actual shift functors and their addition isomorphism.

def splitShift (Phi : C ⥤ C) [Phi.Additive] [Phi.CommShift ℤ]
    (X Z : C) (b d t : ℤ) (split : Phi.obj X ≅ Z⟦b⟧ ⊞ Z⟦b+d⟧) :
    Phi.obj (X⟦t⟧) ≅ Z⟦b+t⟧ ⊞ Z⟦b+d+t⟧ :=
…