We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 820ed60 commit 7f5579bCopy full SHA for 7f5579b
Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
@@ -272,8 +272,8 @@ instance : Linear R (Free R C) where
272
273
theorem single_comp_single {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (r s : R) :
274
(single f r ≫ single g s : Free.of R X ⟶ Free.of R Z) = single (f ≫ g) (r * s) := by
275
- dsimp +instances [CategoryTheory.categoryFree]
276
- simp
+ dsimp +instances [CategoryTheory.categoryFree]
+ simp
277
278
end
279
0 commit comments