LeadingTotalEmbedding.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.DerivedBar.ParityBridge.leadingTotalEmbedding line 28
Source documentation
The exterior D bar is assembled on its actual finite totalization diagonal.
```
def leadingTotalEmbedding (r n : ℕ) :
    (barTotal k D (I r)).X n ⟶ ModuleCat.of D (D ⊗[k] term k A N (r+n)) :=
…
```
Mentions: OAI.DerivedBar.barTotal, OAI.DerivedBar.term
theorem OAI.DerivedBar.ParityBridge.leadingTotalEmbedding_ι line 34
theorem OAI.DerivedBar.ParityBridge.innerIter_eq_explicit line 41
Source documentation
The independently recursive inner total is the previously constructed explicit multibar.
```
theorem innerIter_eq_explicit (r : ℕ) : I r = explicitMultibar k D X r Z := by
…
```
Mentions: OAI.DerivedBar.explicitMultibar