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 _ _