Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - docs: Fix copy’n'pasta in Mathlib/Algebra/Module/LinearMap.lean #2082

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - docs: Fix copy’n'pasta in Mathlib/Algebra/Module/LinearMap.lean #2082

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
f6ea910
[docs] Fix copy’n'pasta in Mathlib/Algebra/Module/LinearMap.lean
nomeata Feb 5, 2023
e845d77
update mathlib 3 rev
nomeata Feb 5, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Module/LinearMap.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro, Anne
Frédéric Dupuis, Heather Macbeth

! This file was ported from Lean 3 source module algebra.module.linear_map
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! leanprover-community/mathlib commit cc8e88c7c8c7bc80f91f84d11adb584bf9bd658f
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
Expand Down Expand Up @@ -933,7 +933,7 @@ theorem comp_neg (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃]
ext fun _ ↦ g.map_neg _
#align linear_map.comp_neg LinearMap.comp_neg

/-- The negation of a linear map is linear. -/
/-- The subtraction of two linear maps is linear. -/
instance : Sub (M →ₛₗ[σ₁₂] N₂) :=
⟨fun f g ↦
{ toFun := f - g
Expand Down