doc(linear_algebra): fix wrong docstring (#10139)

leanprover-community · Nov 3, 2021 · 95cdeba · 95cdeba
1 parent 2b87435
commit 95cdeba
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/linear_algebra/prod.lean b/src/linear_algebra/prod.lean
@@ -141,7 +141,7 @@ theorem inl_injective : function.injective (inl R M M₂) :=
 theorem inr_injective : function.injective (inr R M M₂) :=
 λ _, by simp
 
-/-- The coprod function `λ x : M × M₂, f.1 x.1 + f.2 x.2` is a linear map. -/
+/-- The coprod function `λ x : M × M₂, f x.1 + g x.2` is a linear map. -/
 def coprod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : M × M₂ →ₗ[R] M₃ :=
 f.comp (fst _ _ _) + g.comp (snd _ _ _)