mathlib3
feat(data/polynomial/laurent): degrees for Laurent polynomials
#13415
Open
Overview
Commits
201
Changes
View On GitHub

feat(data/polynomial/laurent): degrees for Laurent polynomials #13415

adomani wants to merge 201 commits into master from adomani_laurent_polynomials
adomani
adomani new file
97d40a08
adomani lint
a7612912
adomani Merge branch 'master' into adomani_laurent_polynomials
08122094
adomani rename file
d836ccbd
adomani cleanup
c4aa948c
adomani lifts of (add_)monoid_algebras
3cb0d1d5
adomani update name
a2369a12
adomani begin switch to semiring
7fba9ddc
adomani Eric's suggestions
c69eff77
adomani fully remove _lift
01f55f99
eric-wieser chore(algebra/monoid_algebra/basic): use the homomorphism typeclasses
0a26f320
eric-wieser lintfix
724fbce6
adomani remove a definition, move a lemma
9a23ef26
eric-wieser fix
e47dba4c
adomani Merge remote-tracking branch 'origin/eric-wieser/monoid_algebra-hom-c…
f2c8e520
adomani move
5a5d6560
adomani Merge remote-tracking branch 'origin/eric-wieser/monoid_algebra-hom-c…
a56ff4cd
adomani with Eric's proofs
1eb16eb8
adomani various fixes, with external lemmas
7fdc1373
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
c97b25ab
adomani remove comment
3839c7ae
adomani doc-module
15e94aa1
adomani lint
3947758a
adomani more lint
3e7e181f
adomani lint
5b468a11
adomani brace
9339377b
leanprover-community-bot-assistant leanprover-community-bot-assistant added blocked-by-other-PR
adomani remove comment
487bc01a
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
0fb597c6
adomani remove unneeded lemmas
932c7f3a
adomani remove unneeded lemmas
538ff02d
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
c8e37464
adomani fix doc-strings
c95a78e2
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
9b08a5de
adomani open finsupp namespace
2a62330b
adomani add back lemmas
89b1d61d
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
2c225ae8
adomani remove unnecessary import
62ef6b25
adomani polynomial.to_laurent_polynomial is injective
26332ec8
adomani use hom_type_classes, following Eric's suggestion
a066ec47
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
82fd1ce4
adomani doc-string + change namespace for injective
89ca510d
adomani rename `exists_X_pow` to `exists_T_pow`
833a3367
adomani remove namespaces + shorten to to_laurent
06bcc36a
adomani simplify
9c0c2928
alexjbest
alexjbest commented on 2022-04-14
adomani T'
e9dd96d5
adomani Alex's doc-string suggestion
916c7de0
adomani space + lint
c1229052
adomani doc-string
ab7fac7e
adomani doc-string
4fea2c89
leanprover-community-bot-assistant leanprover-community-bot-assistant removed blocked-by-other-PR
adomani Merge branch 'master' into adomani_lift_monoid_algebra
92cfd5c4
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
c47a7ee1
adomani Eric's suggestions
b9dd3086
adomani mirror eric's suggestions
fdacc822
adomani Merge branch 'adomani_lift_monoid_algebra' of ssh://github.com/leanpr…
889e8396
adomani small fix
63970cf6
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
eb7d7e32
adomani more fixes
4892698e
adomani use Junyan Xu's suggestions + broken proof
60b387e0
adomani remove lemma
66c95c99
adomani Merge remote-tracking branch 'origin/master' into adomani_lift_monoid…
ee961f0d
adomani lint braces
ac074c85
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
03d316da
adomani Eric's suggestions
326058b4
adomani add_monoid_hom_class
30ef702e
adomani Update src/algebra/monoid_algebra/basic.lean
6ae6cf64
adomani simps and -simp for linter
0b5a6206
adomani doc-string
d03e08ce
adomani rename as per Junyan Xu's comment
ee864bf4
adomani Eric's comments
4a92787a
adomani more improvements from Eric
cfa553aa
adomani Apply suggestions from code review
23dc1b41
adomani add simps tag <-- Eric
8166c51c
adomani doc-strings
2e132a8e
adomani Merge remote-tracking branch 'origin/master' into adomani_lift_monoid…
9a92d6ba
adomani add add twice
92c23a91
adomani Apply suggestions from code review
b85190c0
adomani non_unital
be7ae46e
adomani add
f94410e9
adomani additive
16213bab
adomani Merge branch 'adomani_lift_monoid_algebra' into adomani_laurent_polyn…
0a2ec14f
adomani rename
31ce7075
adomani Merge branch 'master' into adomani_laurent_polynomials
9b2c3873
kim-em kim-em added WIP
eric-wieser
eric-wieser commented on 2022-04-28
eric-wieser
eric-wieser commented on 2022-04-28
adomani adomani removed WIP
adomani adomani added awaiting-review
eric-wieser eric-wieser marked this pull request as ready for review 3 years ago
eric-wieser
eric-wieser commented on 2022-04-28
eric-wieser
eric-wieser commented on 2022-04-28
eric-wieser
eric-wieser commented on 2022-04-28
eric-wieser
eric-wieser commented on 2022-04-28
eric-wieser
eric-wieser commented on 2022-04-28
adomani
adomani commented on 2022-04-29
adomani Eric's changes
e4dae9da
adomani `finsupp.comap_domain` is an `add_monoid_hom`
64377050
eric-wieser
eric-wieser commented on 2022-04-29
adomani remove stuff from later PR
22dd7829
adomani Merge branch 'master' into adomani_laurent_polynomials_defs
5989dd20
eric-wieser
eric-wieser commented on 2022-04-29
adomani end section
4d263992
eric-wieser
eric-wieser commented on 2022-04-29
eric-wieser
eric-wieser commented on 2022-04-29
adomani Merge branch 'master' into adomani_laurent_polynomials
472064dd
leanprover-community-bot-assistant leanprover-community-bot-assistant added blocked-by-other-PR
adomani doc string
7aa7d36f
adomani Merge branch 'adomani_laurent_polynomials_defs' into adomani_laurent_…
26673d8e
adomani re-add removed stuff
6998afa7
adomani Eric's comments
63664b23
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials
c480748f
adomani `trunc` uses `comap_domain` instead of `map_domain`
6c4f24f8
adomani add one lemma, explicit/implicit
56a49843
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials
fba99ab7
adomani updates using Eric's suggestions
d3791f07
adomani maybe smul?
ec2c2e2c
adomani Update src/data/polynomial/laurent.lean
f455771f
adomani Apply suggestions from code review
12eb1f9a
adomani Apply suggestions from code review
9ff4703f
adomani Update src/data/polynomial/laurent.lean
221595fe
adomani add a rfl-lemma
7e4fac9f
adomani Merge branch 'adomani_laurent_polynomials_defs' of ssh://github.com/l…
cb2ad462
adomani remove unneeded types
8a0d514f
adomani Update src/data/polynomial/laurent.lean
0cb7ca39
adomani Merge branch 'adomani_laurent_polynomials_defs' of ssh://github.com/l…
b7f9c9d5
adomani add smul lemma
b04c34bf
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials
19dad816
adomani Merge branch 'adomani_laurent_polynomials_defs' into adomani_laurent_…
95824c6a
adomani update docmodule
c2e4250f
adomani fix and update
a5003c93
adomani golf
72abd94c
adomani move lemma within the file
71d31641
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials
7dcf7760
adomani weaker assumptions
9c40e306
adomani golf
89509fc4
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials
3188bb66
adomani use open add_monoid_algebra
4ee1a080
adomani Merge branch 'adomani_laurent_polynomials_defs' into adomani_laurent_…
27659822
adomani docmodule
9bf3f4a8
adomani fix
c027a281
adomani Merge branch 'adomani_laurent_polynomials_defs' into adomani_laurent_…
1c911c97
adomani golf
71cd8d5c
adomani Merge branch 'master' into adomani_laurent_polynomials_defs
f23281f8
adomani added Riccardo's suggestion
6e8170d8
adomani Merge branch 'adomani_laurent_polynomials_defs' into adomani_laurent_…
f0c93fef
adomani Merge branch 'master' into adomani_comap_hom
f888dfe2
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials
9cb7e7c4
adomani add localization
bf4a42dc
adomani Merge branch 'master' into adomani_laurent_polynomials
86d448b1
adomani adomani changed the title feat(data/polynomial/laurent): define Laurent polynomials and some API feat(data/polynomial/laurent): avoiding algebra instances in Laurent polynomials 3 years ago
adomani Correct def/lemma
a46bbed2
eric-wieser golf and generalize
44971f49
eric-wieser generalize typeclasses
49a5df18
adomani lint
d6e82d83
adomani lint
f898e1f1
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials
e98172be
adomani simplify erw
834555e4
adomani golf
4f4f538d
adomani Merge branch 'master' into adomani_laurent_polynomials
ea2dfc09
adomani remove merged lemma
a01f333c
adomani Merge branch 'master' into adomani_comap_hom
cf6031fd
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials
c22db19c
adomani Merge remote-tracking branch 'origin/master' into adomani_laurent_pol…
0fe75c35
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials_trunc
9dd7b488
adomani add trunc
37f60c4a
adomani add simps support
398acbc6
adomani Update src/data/finsupp/basic.lean
19ce44d6
adomani Merge branch 'adomani_comap_hom' of ssh://github.com/leanprover-commu…
b0e86b58
adomani rcases for obtain
b121c389
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials
4431e9d3
adomani Merge branch 'adomani_comap_hom' into adomani_laurent_polynomials_trunc
89f0be12
adomani Merge branch 'adomani_laurent_polynomials_trunc' into adomani_laurent…
a58bd9f2
adomani add Riccardo's todo
9e6e8a80
adomani add left_inverse
c892370c
adomani Merge branch 'adomani_laurent_polynomials_trunc' into adomani_laurent…
ba4d0462
adomani Merge branch 'master' into adomani_laurent_polynomials
8c5c40e8
adomani add todo `R`-linear map
7c50d44e
adomani Merge branch 'master' into adomani_laurent_polynomials
7d97b040
adomani add exists
f24e4011
adomani Merge branch 'adomani_laurent_polynomials_exists' into adomani_lauren…
682d0d09
adomani Merge branch 'master' into adomani_laurent_polynomials_exists
2beb0302
adomani Update src/data/polynomial/laurent.lean
41035503
adomani Merge branch 'adomani_laurent_polynomials_exists' of ssh://github.com…
00282799
adomani Eric's suggestion
4954ab26
adomani add todo
8a51be18
adomani move T_sub
84d23877
adomani move₂ T_sub
487b7892
adomani Merge branch 'master' into adomani_laurent_polynomials_exists
188f73f0
adomani induction works!
5b41ce15
adomani laurent polynomials are a module over polynomials
ad068a05
adomani Merge branch 'adomani_laurent_polynomials_module' into adomani_lauren…
517298db
adomani Merge branch 'adomani_laurent_polynomials_exists' into adomani_lauren…
fdfc60e2
adomani add degree
40215f7c
adomani fix
278d9b55
adomani Eric's golf
e6abe951
adomani Merge branch 'adomani_laurent_polynomials_module' into adomani_lauren…
bcbc915b
adomani parentheses
6b56abff
adomani two more instance
d25b31da
adomani Merge branch 'adomani_laurent_polynomials_module' into adomani_lauren…
1e95cf62
adomani fixes
b461f244
adomani remove paragraph
1ef22c6d
adomani more of Eric's generalization and golfing
28d00acd
adomani Merge branch 'master' into adomani_laurent_polynomials_module
8132f378
adomani Merge branch 'adomani_laurent_polynomials_module' into adomani_lauren…
81cdc2aa
adomani Merge branch 'master' into adomani_laurent_polynomials_exists
a9ca77d8
adomani Merge branch 'adomani_laurent_polynomials_exists' into adomani_lauren…
7510b7ac
adomani Merge branch 'master' into adomani_laurent_polynomials_exists
b67983ba
adomani merge
5a5b23d5
adomani comment further directions
3b34ca00
adomani Merge branch 'adomani_laurent_polynomials_exists' of ssh://github.com…
567abcdd
adomani Revert "merge"
e3ac672e
adomani Merge branch 'master' into adomani_laurent_polynomials
5cb98d5f
adomani Merge branch 'adomani_laurent_polynomials_exists' into adomani_lauren…
dd9fc92f
adomani Merge branch 'adomani_laurent_polynomials' of ssh://github.com/leanpr…
a22c7117
adomani Merge branch 'master' into adomani_laurent_polynomials
ad17879a
mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed blocked-by-other-PR
leanprover-community leanprover-community deleted a comment from leanprover-community-bot-assistant on 2022-05-31
adomani localization
974c4ecf
adomani Merge branch 'adomani_laurent_localization' into adomani_laurent_poly…
78ce74d7
adomani remove duplicated import
c44a5871
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed blocked-by-other-PR
mathlib-dependent-issues-bot
adomani adomani removed awaiting-review
adomani adomani added WIP
adomani begin degree
521baacd
adomani Merge branch 'master' into adomani_laurent_polynomials
e9b159d1
adomani adomani changed the title feat(data/polynomial/laurent): avoiding algebra instances in Laurent polynomials feat(data/polynomial/laurent): degrees for Laurent polynomials 3 years ago
kim-em kim-em added too-late

Login to write a write a comment.

Login via GitHub

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