-
Notifications
You must be signed in to change notification settings - Fork 297
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.
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
[Merged by Bors] - feat(linear_algebra/pi_tensor_product): define the tensor product of an indexed family of semimodules #5311
Conversation
Note that as mentioned on zulip, |
#5385 is using |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is some very elegant code. I suggest some very minor things.
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you so much! This looks very clean. I thought that two lemmas could be tagged with simp. Or does the simp-linter disagree?
bors d+
✌️ dupuisf can now approve this pull request. To approve and merge a pull request, simply reply with |
section semiring | ||
|
||
variables {ι : Type*} {R : Type*} [comm_semiring R] | ||
variables {R' : Type*} [comm_semiring R'] [algebra R' R] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Requiring algebra
feels quite strict here. Was is_scalar_tower
not enough?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I could probably do it with [semimodule R' R] [is_scalar_tower R' R R]
, but isn't that just equivalent to algebra anyway?
Ok, thanks for looking into those simp attributes. bors merge |
…an indexed family of semimodules (#5311) This PR defines the tensor product of an indexed family `s : ι → Type*` of semimodules over commutative semirings. We denote this space by `⨂[R] i, s i` and define it as `free_add_monoid (R × Π i, s i)` quotiented by the appropriate equivalence relation. The treatment follows very closely that of the binary tensor product in `linear_algebra/tensor_product.lean`. Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This PR defines the tensor product of an indexed family
s : ι → Type*
of semimodules over commutative semirings. We denote this space by⨂[R] i, s i
and define it asfree_add_monoid (R × Π i, s i)
quotiented by the appropriate equivalence relation. The treatment follows very closely that of the binary tensor product inlinear_algebra/tensor_product.lean
.Zulip thread