Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(ring_theory/tensor_product): add missing scalar tower instances#19143

Closed
eric-wieser wants to merge 6 commits intomasterfrom
eric-wieser/tensor_product-tower-instances
Closed

[Merged by Bors] - feat(ring_theory/tensor_product): add missing scalar tower instances#19143
eric-wieser wants to merge 6 commits intomasterfrom
eric-wieser/tensor_product-tower-instances

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented Jun 2, 2023 •
edited by github-actions bot
Loading

@eric-wieser eric-wieser added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jun 2, 2023
@github-actions github-actions bot added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Jun 2, 2023
@ghost ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 2, 2023
@eric-wieser eric-wieser mentioned this pull request Jun 2, 2023
Closed
@ghost ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 2, 2023
@ghost
Copy link
Copy Markdown

ghost commented Jun 2, 2023

This PR/issue depends on:

@eric-wieser eric-wieser force-pushed the eric-wieser/tensor_product-tower-instances branch from 45aac93 to 4b145b5 Compare June 2, 2023 10:34
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 12, 2023
@eric-wieser eric-wieser added t-algebra Algebra (groups, rings, fields etc) not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 labels Jul 12, 2023
@riccardobrasca riccardobrasca self-assigned this Jul 19, 2023
@eric-wieser eric-wieser mentioned this pull request Jul 21, 2023
Closed
3 tasks
riccardobrasca
riccardobrasca approved these changes Jul 23, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, thanks!

bors d+

src/ring_theory/tensor_product.lean
mul_assoc' mul (by { intros, simp only [mul_apply, mul_assoc], }) x y z

lemma one_mul (x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x :=
protected lemma one_mul (x : A ⊗[R] B) : mul (1 ⊗ₜ 1) x = x :=
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca Jul 23, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe simp?

Copy link
Copy Markdown
Member Author

@eric-wieser eric-wieser Jul 23, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I don't think it's worth it; mul isn't really the simp-normal form anyway.

src/ring_theory/tensor_product.lean
end

lemma mul_one (x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x :=
protected lemma mul_one (x : A ⊗[R] B) : mul x (1 ⊗ₜ 1) = x :=
Copy link
Copy Markdown
Member

@riccardobrasca riccardobrasca Jul 23, 2023

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same here.

@bors
Copy link
Copy Markdown

bors bot commented Jul 23, 2023

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 23, 2023
eric-wieser
eric-wieser commented Jul 23, 2023
View reviewed changes
Copy link
Copy Markdown
Member Author

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 23, 2023
bors bot pushed a commit that referenced this pull request Jul 23, 2023
@eric-wieser
feat(ring_theory/tensor_product): add missing scalar tower instances (#…
88fcdc3 
…19143)
@bors
Copy link
Copy Markdown

bors bot commented Jul 23, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat(ring_theory/tensor_product): add missing scalar tower instances [Merged by Bors] - feat(ring_theory/tensor_product): add missing scalar tower instances Jul 23, 2023
@bors bors bot closed this Jul 23, 2023
@bors bors bot deleted the eric-wieser/tensor_product-tower-instances branch July 23, 2023 12:22
eric-wieser added a commit to leanprover-community/mathlib4 that referenced this pull request Jul 24, 2023
@eric-wieser
chore(linear_algebra/tensor_algebra): forward-port leanprover-communi…
8430455 
…ty/mathlib3#19143
bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jul 27, 2023
@eric-wieser
chore(linear_algebra/tensor_product): forward-port leanprover-communi…
00269a6 
…ty/mathlib3#19143 (#6094)
adomani pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jul 28, 2023
@eric-wieser @adomani
chore(linear_algebra/tensor_product): forward-port leanprover-communi…
c4859d2 
…ty/mathlib3#19143 (#6094)
kim-em pushed a commit to leanprover-community/mathlib4 that referenced this pull request Aug 14, 2023
@eric-wieser @kim-em
chore(linear_algebra/tensor_product): forward-port leanprover-communi…
7ccbb1d 
…ty/mathlib3#19143 (#6094)
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@riccardobrasca riccardobrasca riccardobrasca approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@riccardobrasca riccardobrasca

Labels

delegated The PR author may merge after reviewing final suggestions. modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-algebra Algebra (groups, rings, fields etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@eric-wieser @riccardobrasca @leanprover-community-bot-assistant