OAI/Algebra/Finitistic/Selected/SelectedBarResolution.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.SelectedBarResolution.resolution line 12

   Source documentation

   The genuine absolute bar projective resolution of each actual inflated module. It can have infinitely many nonzero degrees.

   def resolution (Y : FiniteSelectionFamily.S.{0}) : ProjectiveResolution (module Y) :=
   …

2. theorem OAI.LittleFinitistic.SelectedBarResolution.finite_free line 15