Skip to content

Commit

Permalink
fix doc for LinearMap.compRight (#9997)
Browse files Browse the repository at this point in the history
minor typo here. An (f : M2 -> M3) induces a linear map from (M->M2) to (M->M3). Not to (M2 -> M3).

Co-authored-by: Alex Meiburg <[email protected]>
  • Loading branch information
Timeroot and Timeroot committed Jan 25, 2024
1 parent 47a9066 commit 1f2e586
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Module/LinearMap.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 _ _
Expand Down

0 comments on commit 1f2e586

Please sign in to comment.