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 Algebra.Module.LinearMap #1587

Closed
wants to merge 9 commits into from
Closed

[Merged by Bors] - feat: port Algebra.Module.LinearMap #1587

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
2c78446
feat: port Algebra.Module.LinearMap
Vierkantor Jan 16, 2023
6b81eb2
Initial file copy from mathport
Vierkantor Jan 16, 2023
5342fac
Mathbin -> Mathlib; add import to Mathlib.lean
Vierkantor Jan 16, 2023
a367212
WIP: works until the Ring instance
Vierkantor Jan 16, 2023
f9023fe
More fixing; works except for timeouts in `ext_ring_op` and `Module.E…
Vierkantor Jan 17, 2023
7946a03
Revert expansion, now it works again for some reason
Vierkantor Jan 17, 2023
901f7dc
<= 100
qawbecrdtey Jan 20, 2023
d27c19c
Fix names
Vierkantor Jan 20, 2023
da3d315
Fix naming convention
Vierkantor Jan 20, 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
Expand Up @@ -69,6 +69,7 @@ import Mathlib.Algebra.Homology.ComplexShape
import Mathlib.Algebra.Invertible
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.Module.Hom
import Mathlib.Algebra.Module.LinearMap
import Mathlib.Algebra.Module.Pi
import Mathlib.Algebra.Module.PointwisePi
import Mathlib.Algebra.Module.Prod
Expand Down