OAI/Algebra/Finitistic/Bar/BarAdditive.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DerivedBar.termMap_add line 14

   Source documentation

   Each iterated free bar term preserves addition of maps.

   theorem termMap_add (f g : V →ₗ[D] W) (n : ℕ) :
       termMap k D V W (f+g) n = termMap k D V W f n + termMap k D V W g n := by
   …

   Mentions: OAI.DerivedBar.termMap

2. instance OAI.DerivedBar.barFunctor_additive line 30
3. instance OAI.DerivedBar.BimoduleTensor.twoSidedBarFunctor_additive line 42