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

feat(ring_theory/graded_algebra): mv_polynomial is ℕ-graded #10119

Open
wants to merge 134 commits into
base: master
Choose a base branch
from
Open

feat(ring_theory/graded_algebra): mv_polynomial is ℕ-graded #10119

wants to merge 134 commits into from

Conversation

jjaassoonn
Copy link
Collaborator

@jjaassoonn jjaassoonn commented Nov 2, 2021 •
edited by github-actions bot

jjaassoonn and others added 18 commits November 2, 2021 14:20
lemma about homogeneous polynomial
3dbe1b9
definition of graded ring
54d8ac3
projection map of graded ring
19a7b07
recompose_of
d1a0a74
@jjaassoonn @eric-wieser
Update src/ring_theory/graded_ring/basic.lean
03032b3 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
typo
0bb7e90
change graded_ring to graded_ring.core
c835cc2
Merge branch 'graded_ring_dep_2' into graded_ring_dep_3
010c24a
homogeneous elements
8397d47
@jjaassoonn @eric-wieser
Update src/ring_theory/graded_ring/basic.lean
42ff93b 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
shorten proof
c4f5af8
Merge branch 'graded_ring_dep_2' of https://github.com/leanprover-com…
70753d2 
…munity/mathlib into graded_ring_dep_2
fixes
7645bdb
add direct_sum.subgroup_coe_ring_hom
3c14352
add direct_sum.subgroup_coe_ring_hom
91e59aa
delete lint
033988a
Merge branch 'graded_ring_dep_1' into graded_ring_dep_5
3402961
mv_polynomial is graded
db82569
@github-actions github-actions bot 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 Nov 2, 2021
@jjaassoonn jjaassoonn changed the title feat(ring_theory/graded_ring): mv_polynomial is graded by (λ i : ℕ, (homogeneous_submodule σ R i).to_add_subgroup) feat(ring_theory/graded_ring): mv_polynomial is ℕ-graded Nov 2, 2021
@jjaassoonn jjaassoonn mentioned this pull request Nov 2, 2021
Closed
8 tasks
@jjaassoonn jjaassoonn changed the title feat(ring_theory/graded_ring): mv_polynomial is ℕ-graded feat(ring_theory/graded_algebra): mv_polynomial is ℕ-graded Dec 13, 2021
@jjaassoonn
Copy link
Collaborator Author

This likely overlaps a lot with #8913; once the dependencies clear up, we should compare the approaches.

The two induction lemmas in #8913 seems very useful. The map mv_polynomial sigma R \to \Oplus i, homogensou_submodule sigma R in this pr isn't very informative.

@eric-wieser
Copy link
Member

I merged master to make the diff smaller

@leanprover-community-bot-assistant leanprover-community-bot-assistant 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 Mar 4, 2022
@leanprover-community-bot-assistant
Copy link
Collaborator

This PR/issue depends on:

@leanprover-community leanprover-community deleted a comment from github-actions bot Mar 4, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 4, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 5, 2022
@semorrison semorrison added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 8, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 13, 2022
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Mar 28, 2022
@jjaassoonn jjaassoonn added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 28, 2022
@jjaassoonn jjaassoonn removed the awaiting-review The author would like community review of the PR label Jul 19, 2022
@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes merge-conflict Please `git merge origin/master` then a bot will remove this label. awaiting-CI The author would like to see what CI has to say before doing more work. labels Mar 29, 2023
@semorrison semorrison added the too-late This PR was ready too late for inclusion in mathlib3 label Jul 16, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI The author would like to see what CI has to say before doing more work. merge-conflict Please `git merge origin/master` then a bot will remove this label. too-late This PR was ready too late for inclusion in mathlib3
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@jjaassoonn @eric-wieser @leanprover-community-bot-assistant @semorrison