OAI/Algebra/Finitistic/Bar/IndexedPatternEmbedding.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.ParityBridge.eqToHom_tensor_tmul line 32
2. theorem OAI.DerivedBar.ParityBridge.eqToHom_outer_tmul line 39
3. theorem OAI.DerivedBar.ParityBridge.indexedInclusion_toList line 47

   Source documentation

   The old indexed inclusion and old list-pattern embedding agree; transports come solely from the proved equality of their tensor objects and their degrees.

   theorem indexedInclusion_toList {n r : ℕ} (p : Multibar.Indexed.Shape n r)
       (v : Multibar.Indexed.tensor k D X N p) :
       Multibar.Indexed.inclusion k D X N p v =
         termCast k D X N (Multibar.Indexed.length_toList p)
           (embed k D X N (Multibar.Indexed.toList p)
             ((eqToHom (Multibar.Indexed.tensor_toList k D X N p)).hom v)) := by
   …

   Mentions: OAI.DerivedBar.Multibar.Indexed.Shape, OAI.DerivedBar.Multibar.Indexed.tensor, OAI.DerivedBar.Multibar.Indexed.inclusion, OAI.DerivedBar.ParityBridge.termCast, OAI.DerivedBar.Multibar.Indexed.length_toList, OAI.DerivedBar.Multibar.Indexed.toList, OAI.DerivedBar.Multibar.Indexed.tensor_toList

4. theorem OAI.DerivedBar.ParityBridge.outerInclusion_toList line 90
5. theorem OAI.DerivedBar.ParityBridge.outerInclusion_pattern line 109