OAI/Algebra/Finitistic/Bar/RecursiveSuffixTotal.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.ParityBridge.innerTotalEmbedding line 28

   Source documentation

   The same canonical embedding on the actual recursive total, through the previously proved finite-sum flattening.

   def innerTotalEmbedding (r n : ℕ) :
       (RecursiveTotal.iter B Z r).X n →ₗ[k] term k A N (r+n) :=
   …

   Mentions: OAI.DerivedBar.RecursiveTotal.iter, OAI.DerivedBar.term

2. theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_assemble line 33
3. theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_differential line 43
4. theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_smul line 56
5. theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_ideal_zero line 67
6. theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_bottom line 72
7. theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_inclusion line 77
8. theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_zero line 85
9. theorem OAI.DerivedBar.ParityBridge.innerTotalEmbedding_zero_succ line 92