OAI/Algebra/Finitistic/Rectification/FinalGradedAcyclic.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.FinalGradedAcyclic.grade0_vertex2_acyclic line 20

   Source documentation

   The original source-zero quotient at vertex two is acyclic, with every relation column retained.

   theorem grade0_vertex2_acyclic :
       ((RelationVertexCoordinates.vertex P).obj (Exactness.G0 s D₀ D₁ D₂ f g)).Acyclic := by
   …

   Mentions: OAI.LittleFinitistic.RelationVertexCoordinates.vertex