OAI/Algebra/Finitistic/Bar/FiniteSumSupport.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DerivedBar.RecursiveTotal.supportIso line 14

   Source documentation

   Omitting zero summands is an isomorphism of ordinary direct sums.

   def supportIso (hzero : ∀ i, ¬P i → IsZero (V i)) :
       ModuleCat.of D (⨁ i, V i) ≅ ModuleCat.of D (⨁ i : {i // P i}, V i.val) where
   …