From 1c40517ed8127c65df4dff21aa327e45b58dd994 Mon Sep 17 00:00:00 2001 From: Alex Meiburg Date: Fri, 26 Jan 2024 00:01:33 +0800 Subject: [PATCH] fix docs --- Mathlib/Algebra/Module/LinearMap.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index 6ebe521a7f4d6..b51fbccc968d7 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -1444,7 +1444,7 @@ variable [Module R M] [Module R M₂] [Module R M₃] variable (f g : M →ₗ[R] M₂) /-- Composition by `f : M₂ → M₃` is a linear map from the space of linear maps `M → M₂` -to the space of linear maps `M₂ → M₃`. -/ +to the space of linear maps `M → M₃`. -/ def compRight (f : M₂ →ₗ[R] M₃) : (M →ₗ[R] M₂) →ₗ[R] M →ₗ[R] M₃ where toFun := f.comp map_add' _ _ := LinearMap.ext fun _ => map_add f _ _