mathlib3
feat(ring_theory/mv_polynomial/homogeneous): Multivariate polynomials permit a nat-grading
#8913
Open
Overview
Commits
41
Changes
View On GitHub

feat(ring_theory/mv_polynomial/homogeneous): Multivariate polynomials permit a nat-grading #8913

eric-wieser wants to merge 41 commits into master from eric-wieser/homogenous-direct_sum-phase-2
eric-wieser
eric-wieser Attempt a direct sum of graded algebras
8f81637a
eric-wieser feat(ring_theory/polynomial/homogenous): add a `direct_sum.gcomm_mono…
ef572ecc
eric-wieser feat(ring_theory/polynomial/homogenous): Attempt to define the isomor…
38b34c15
eric-wieser Merge branch 'master' of github.com:leanprover-community/mathlib into…
5e493c0f
eric-wieser wip
ab26d0f8
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/direct_…
a56500f9
eric-wieser feat(algebra/direct_sum): graded algebras
5a104822
eric-wieser remove simps
466fca7b
eric-wieser just use simps instead
fac7bf2e
eric-wieser golf
70ec9158
eric-wieser fix CI
95b3e040
eric-wieser Update src/algebra/direct_sum_graded_algebra.lean
ac4674a9
eric-wieser Rename src/algebra/direct_sum_graded_algebra.lean to src/algebra/dire…
f8f1f955
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/direct_…
88cdcccb
eric-wieser Review comments, replace a def with an instance
365533cb
eric-wieser Use the new instance
e64ff957
eric-wieser Update TODO
d083a706
eric-wieser Merge branch 'eric-wieser/direct_sum_graded.algebra' into eric-wieser…
1c9ddf6b
eric-wieser Add ext lemmas
4d1725e0
eric-wieser Switch to alg_homs
b0f07b3c
eric-wieser wip
e53d5785
eric-wieser Add ext lemmas
5558fe8b
eric-wieser Merge branch 'eric-wieser/direct_sum_graded.algebra' into eric-wieser…
33e63b80
eric-wieser Finished!
e511d0d5
eric-wieser Spelling errors
cdcdeb34
github-actions github-actions added blocked-by-other-PR
eric-wieser Tidy up
05d96ca7
eric-wieser eric-wieser added RFC
eric-wieser eric-wieser requested a review from jcommelin jcommelin 4 years ago
eric-wieser fix(ring_theory/polynomial/homogeneous): spelling mistake in `homogen…
0c65647c
github-actions github-actions added merge-conflict
eric-wieser eric-wieser changed the title feat(ring_theory/mv_polynomial/homogeneous): Multlivariate polynomials permit a nat-grading feat(ring_theory/mv_polynomial/homogeneous): Multivariate polynomials permit a nat-grading 4 years ago
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/add-the…
5fab0dee
eric-wieser Merge branch 'eric-wieser/add-the-missing-e' into eric-wieser/homogen…
06bb5ae1
github-actions github-actions removed merge-conflict
eric-wieser golf
4bcf805e
jcommelin
eric-wieser Merge branch 'master' into eric-wieser/homogenous-direct_sum-phase-2
ff256a83
github-actions github-actions removed blocked-by-other-PR
eric-wieser
eric-wieser commented on 2021-08-29
kbuzzard
eric-wieser
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/homogen…
ebdfdfd4
eric-wieser wip
669e1a7f
eric-wieser Revert "wip"
1ab82779
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/homogen…
8adb0871
eric-wieser chore(algebra/direct_sum/internal): add missing simp lemmas
ad56baa9
eric-wieser fixups
9f363e73
jcommelin
jcommelin commented on 2021-11-04
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/homogen…
11df251f
github-actions
jcommelin jcommelin added awaiting-author
leanprover-community-bot-assistant leanprover-community-bot-assistant added merge-conflict
eric-wieser Merge remote-tracking branch 'origin/master' into eric-wieser/homogen…
42c6b457
leanprover-community-bot-assistant leanprover-community-bot-assistant removed merge-conflict
eric-wieser Use new defs
c1699585
eric-wieser golf
9a43dade
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
RFC awaiting-author too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum