feat(ring_theory/graded_algebra): `mv_polynomial` is ℕ-graded #10119
jjaassoonn
wants to merge
134 commits into
master
from
graded_ring_dep_5
lemma about homogeneous polynomial
3dbe1b9c
definition of graded ring
54d8ac31
projection map of graded ring
19a7b078
recompose_of
d1a0a74e
Update src/ring_theory/graded_ring/basic.lean
03032b33
typo
0bb7e902
change `graded_ring` to `graded_ring.core`
c835cc27
Merge branch 'graded_ring_dep_2' into graded_ring_dep_3
010c24a5
homogeneous elements
8397d47e
Update src/ring_theory/graded_ring/basic.lean
42ff93bb
shorten proof
c4f5af8b
Merge branch 'graded_ring_dep_2' of https://github.com/leanprover-com…
70753d2f
fixes
7645bdba
add `direct_sum.subgroup_coe_ring_hom`
3c14352a
add `direct_sum.subgroup_coe_ring_hom`
91e59aae
delete `lint`
033988af
Merge branch 'graded_ring_dep_1' into graded_ring_dep_5
34029612
`mv_polynomial` is graded
db825691
jjaassoonn
changed the title 
refactor(algebra/direct_sum): rework internally-graded objects
42a96000
fix
06dff2ef
canonical maps
19935269
docstrings
53385f58
fix
d6605bd0
Merge branch 'eric-wieser/graded_subobjects' into graded_ring_dep_2
65f253f4
lint and docs
da81f24c
merge @eric-wieser's pr and changed accordinhly
d13bfacb
Deleted duplicated authors
648910d0
Merge branch 'eric-wieser/graded_subobjects' into graded_ring_dep_2
8117c1fa
change a lemma used in a proof
3a469b8a
Merge branch 'master' into graded_ring_dep_2
ae33ee42
Merge remote-tracking branch 'origin/master' into graded_ring_dep_2
212ebbdf
change to graded algebra
849356f9
changed graded_ring to graded algebra every where
af874be5
commit
554ff4ea
fix
2f2b0164
update doc_string
c7207576
Apply suggestions from code review
91d78de6
Apply suggestions from code review
2aac9adb
Apply suggestions from code review
31c10146
fix
13e20b68
Update src/ring_theory/graded_algebra/basic.lean
bd9f1cdf
change decompose to decompose' but keep recompose
c263ce62
apply suggestion from @eric-wieser
9d712651
Update basic.lean
e1aae1c4
Update src/ring_theory/graded_algebra/basic.lean
d435d711
Merge branch 'graded_ring_dep_2' into graded_ring_dep_3
cc298628
change to graded_algebra
a633f1d3
Merge branch 'master' into graded_ring_dep_3
703ca0ba
change to linear map and simplified proof.
9a17bcc8
Merge branch 'graded_ring_dep_3' of https://github.com/leanprover-com…
26d3a839
apply suggestion from eric
a698cf8c
better definition by @eric-wieser
0c35d0fd
Update src/ring_theory/graded_algebra/basic.lean
40ab6ca5
Update src/ring_theory/graded_algebra/basic.lean
fe298b4c
combine pr and used @eric-wieser much nicer proof
11070fbc
shorten line
a5b3bccf
formatting
57d0ea16
Update src/ring_theory/graded_algebra/basic.lean
849625c4
Update src/ring_theory/graded_algebra/basic.lean
064a7678
shorten proof
bb7ca3b3
apply suggestion from @eric-wieser
61056809
coercion problem
c07eb97c
try to add @eric-wieser's helper lemma, but it doesn't compile
c4408898
mul_decompose
abb8500a
Update src/ring_theory/graded_algebra/basic.lean
13b64bf6
move things around to make linter happy
0bf5c0f4
add helper lemma and shorten proof as propsed by @eric-wieser
05be9005
`direct_sum.coe_mul_apply_submodule`
c101ca28
linter
2a3451d4
moved around
6e1bdbd1
doc string
e7a1dee1
Apply suggestions from code review
1136cec5
let's see if this comp
05908879
linting
3b197616
fix
2b7574a3
added missing lemma
6094f3cd
remove unnecessary lemma
fece57e0
fix?
3fb5d8d5
this should fix it
692ae2e8
Update basic.lean
84579b2d
moved things around
c80995df
Merge branch 'master' into graded_ring_dep_4
43d5acfa
Merge remote-tracking branch 'origin/master' into graded_ring_dep_4
3a74f9e8
Merge branch 'graded_ring_dep_3' into graded_ring_dep_4
9e7e72a8
I need to wait for this be cached, otherwise nothign compiles
94a38bf1
homogeneous_element
7465b147
Merge remote-tracking branch 'origin/master' into graded_ring_dep_4
36b46cf7
remove group_theory change
5f95dfc5
indentation
4b88db2f
apply suggestions from @eric-wieser
567f2a89
Update src/algebra/graded_monoid.lean
2dab0d07
Update src/algebra/graded_monoid.lean
c0bb693e
Update src/algebra/graded_monoid.lean
b66840c2
fix import
04326043
Merge remote-tracking branch 'origin/master' into graded_ring_dep_4
277689b3
Merge branch 'graded_ring_dep_4' into graded_ring_dep_5
43558b3b
Update src/ring_theory/graded_algebra/basic.lean
fdfd8297
linter
95ee79e3
fix import?
cd8993ba
Merge remote-tracking branch 'origin/master' into graded_ring_dep_5
08217d1f
Merge branch 'graded_ring_dep_5' of https://github.com/leanprover-com…
728e2048
Merge remote-tracking branch 'origin/master' into graded_ring_dep_5
8222a533
just put it here for now
591e222a
Merge branch 'graded_ring_dep_5' of https://github.com/leanprover-com…
8ca62127
Delete homogeneous_ideal.lean
b43c901e
apply suggestion from @eric-wieser
4c512bb8
is linter happy?
33b804e5
Update src/algebra/direct_sum/internal.lean
fb614054
Apply suggestions from code review
2c224a35
update name
630ea2be
delete exists.some and moved things around
d007c731
linter what do you think
587edf84
Update src/algebra/direct_sum/internal.lean
8da6648b
apply suggestion from eric
03af3741
Update src/algebra/direct_sum/internal.lean
92f245e1
Apply suggestions from code review
c0e9a7a3
update doc string
2fe00bdc
Merge branch 'graded_ring_dep_4' of https://github.com/leanprover-com…
b0529045
Merge branch 'graded_ring_dep_4' into graded_ring_dep_5
b2551a96
recovering
4037c5fd
finished
e63035cb
t
14cfd543
delete classical
17687388
linter
a3076727
jjaassoonn
changed the title
Merge remote-tracking branch 'origin/master' into graded_ring_dep_5
ecd5d17f
Merge remote-tracking branch 'origin/master' into graded_ring_dep_5
c1d93c30
merge master
4f0f549c
Merge remote-tracking branch 'origin/master' into graded_ring_dep_5
a67615b2
cleanup
34562916
minor cleanup
69295fdd
minor golf
6ba1d3fb
minor golf
78c482ac
docstring
539fdbe7
Update mv_polynomial.lean
157cf9e0
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-author
merge-conflict
awaiting-CI
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub