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] - feat: port LinearAlgebra.Finsupp #2277

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat: port LinearAlgebra.Finsupp #2277

Show file tree
Hide file tree
Changes from 7 commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
720ef19
feat: port LinearAlgebra.Finsupp
jcommelin Feb 14, 2023
674df28
Initial file copy from mathport
jcommelin Feb 14, 2023
2bc67b8
automated fixes
jcommelin Feb 14, 2023
c6954fb
remove some empty lines
jcommelin Feb 14, 2023
0c5028d
fix most of first 300 lines
jcommelin Feb 14, 2023
d55d9c8
fix a few more lines
jcommelin Feb 14, 2023
da30ece
small fix.
qawbecrdtey Feb 15, 2023
4e805ff
simple fixes
LukasMias Feb 16, 2023
bdb8d40
relatively easy fixes
LukasMias Feb 16, 2023
ef8fb97
Merge branch 'master' into port/LinearAlgebra.Finsupp
Komyyy Feb 17, 2023
3156201
fix LinearMap.coe_mk
Komyyy Feb 17, 2023
bc5ae50
51 red errors left
Komyyy Feb 17, 2023
9b58134
align
Komyyy Feb 17, 2023
a9c2330
simplex fixes plus docstrings
LukasMias Feb 17, 2023
50e397b
fix AAHRG
Komyyy Feb 17, 2023
b2f9c0a
fix
Komyyy Feb 17, 2023
40781b4
porting note
Komyyy Feb 17, 2023
92d4075
notation of LinearEquiv.trans
Komyyy Feb 17, 2023
31bb26a
fix Finsupp.congr
Komyyy Feb 17, 2023
10efbc1
other PRs
Komyyy Feb 17, 2023
f37c4c3
13 red errors left
Komyyy Feb 17, 2023
a910907
no errors & script lints anymore
Komyyy Feb 18, 2023
43a5b8a
no build lints anymore
Komyyy Feb 18, 2023
3863a21
naming conventions & edit docs & pi notations
Komyyy Feb 18, 2023
af62340
other PR
Komyyy Feb 18, 2023
96fb615
indent
Komyyy Feb 18, 2023
e079b6c
Merge branch 'master' into port/LinearAlgebra.Finsupp
Komyyy Feb 19, 2023
c6ceb4a
Merge branch 'master' into port/LinearAlgebra.Finsupp
Komyyy Feb 21, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
1 change: 1 addition & 0 deletions Mathlib.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -779,6 +779,7 @@ import Mathlib.Lean.Meta
import Mathlib.Lean.Meta.Simp
import Mathlib.LinearAlgebra.AffineSpace.Basic
import Mathlib.LinearAlgebra.Basic
import Mathlib.LinearAlgebra.Finsupp
import Mathlib.LinearAlgebra.GeneralLinearGroup
import Mathlib.LinearAlgebra.Pi
import Mathlib.LinearAlgebra.Span
Expand Down