C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + (𝟙 K[X] - P q) = 𝟙 K[X]
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + Q q = 𝟙 K[X]
rw [Q]
no goals
C : Type u_2
inst✝¹ : Category C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ P q + (𝟙 K[X] - P q) = 𝟙 K[X]
abel