PR #4321 feat(algebra/free_algebra): Define a grading

feat(algebra/free_algebra): Define a grading #4321

eric-wieser wants to merge 41 commits into master from eric-wieser/free_algebra-grading

eric-wieser added WIP

eric-wieser added blocked-by-other-PR

eric-wieser changed the title ~~feat(algebra/free_algebra): Attempt to define a grading~~ feat(algebra/free_algebra): Attempt to define a grading (deps: #4315) 5 years ago

eric-wieser commented on 2020-09-29

eric-wieser removed WIP

eric-wieser added awaiting-review

eric-wieser marked this pull request as ready for review 5 years ago

rwbarton commented on 2020-09-30

rwbarton removed awaiting-review

rwbarton added awaiting-author

eric-wieser changed the base branch from master to eric-wieser/monoid_algebra-tweaks 5 years ago

github-actions added merge-conflict

eric-wieser changed the title ~~feat(algebra/free_algebra): Attempt to define a grading (deps: #4315)~~ feat(algebra/free_algebra): Attempt to define a grading (deps: #4315, #4365) 5 years ago

feat(algebra/free_algebra): Add an inductive principle

957b4838

chore(algebra/free_algebra): Use a subtype instead of a struct

e7897028

chore(algebra/free_algebra): Disable false positive linter

87d31ffb

chore(algebra/free_algebra): Tidy up coercions

778e9db8

eric-wieser force pushed from ad8308a1 to a66671eb 5 years ago

github-actions removed merge-conflict

refactor(algebra/free_algebra): Replace most of the code with subalgebra

67e8211f

fix(*): remove squeeze_simp

28b18930

Merge remote-tracking branch 'origin/master' into eric-wieser/free_al…

ed419ec1

chore(*): Tidy the proof

d816bfa6

Add induction for the exterior algebra too

aff14869

feat(data/monoid_algebra): Add missing has_coe_to_fun instance

9f22aa68

feat(algebra/free_algebra): Attempt to define a grading

e75b7ef9

Death throes of a failed attempt

21ca265e

feat(algebra/free_algebra): A few lemmas about grades of free algebras

62a77f0c

github-actions added merge-conflict

chore(*): Remove duplication between `sum_id` and `lift`

fd54b8d4

eric-wieser force pushed from a66671eb to fd54b8d4 5 years ago

github-actions removed merge-conflict

fix(*): Solve merge mistake

234ff720

wip

eec3c2b6

chore(algebra/monoid_algebra): Replace `algebra_map'` with `single_(z…

81aa68b0

Merge branch 'eric-wieser/single-hom' into eric-wieser/free_algebra-g…

f999d1ac

wip

abaa760e

wip

b63b36c9

eric-wieser changed the base branch from eric-wieser/monoid_algebra-tweaks to master 5 years ago

Merge branch 'eric-wieser/free_algebra-induction' into eric-wieser/fr…

e5b725e3

Revert unrelated changes

b702aab1

Merge branch 'master' of github.com:leanprover-community/mathlib into…

51900f90

Fix bad merge

5489c462

Merge remote-tracking branch 'origin/master' into eric-wieser/free_al…

3ce401d8

wip

38d3e48f

feat(algebra/algebra/basic): Add `map_finsupp_(sum|prod)` to `alg_(ho…

082ca79d

Merge branch 'eric-wieser/alg_hom.map_finsupp_sum' into eric-wieser/f…

99b4ac1c

Cleanup some more

303117df

eric-wieser changed the title ~~feat(algebra/free_algebra): Attempt to define a grading (deps: #4315, #4365)~~ feat(algebra/free_algebra): Define a grading (deps: #4315, #4365) 5 years ago

feat(algebra/algebra/basic): Add `map_finsupp_(sum|prod)` to `alg_(ho…

40b1eb81

Merge branch 'eric-wieser/alg_hom.map_finsupp_sum' into eric-wieser/f…

1a5eaa93

eric-wieser changed the title ~~feat(algebra/free_algebra): Define a grading (deps: #4315, #4365)~~ feat(algebra/free_algebra): Define a grading (deps: #4315, #4603) 5 years ago

Fix the proof

06e16f59

github-actions added merge-conflict

jcommelin changed the title ~~feat(algebra/free_algebra): Define a grading (deps: #4315, #4603)~~ feat(algebra/free_algebra): Define a grading (deps: #4315) 5 years ago

Merge remote-tracking branch 'origin/master' into eric-wieser/free_al…

9c419699

github-actions removed merge-conflict

eric-wieser removed awaiting-author

eric-wieser added awaiting-review

eric-wieser commented on 2020-10-19

Cleanup the proofs

2d979c33

kim-em changed the title ~~feat(algebra/free_algebra): Define a grading (deps: #4315)~~ feat(algebra/free_algebra): Define a grading 5 years ago

kim-em removed blocked-by-other-PR

Merge remote-tracking branch 'origin/master' into eric-wieser/free_al…

bee9b3c5

eric-wieser commented on 2020-10-20

Update src/algebra/monoid_algebra.lean

caaa54d4

github-actions added merge-conflict

kbuzzard commented on 2020-10-22

Merge remote-tracking branch 'origin/master' into eric-wieser/free_al…

33f38c70

wip

db820597

eric-wieser added blocked-by-other-PR

Merge branch 'master' of github.com:leanprover-community/mathlib into…

986ed3c1

github-actions removed merge-conflict

fix(*): adjust for changed lemmas

1d0b9c99

eric-wieser removed blocked-by-other-PR

eric-wieser force pushed from 72745022 to 1d0b9c99 5 years ago

jcommelin requested a review from

rwbarton 5 years ago

github-actions added merge-conflict

Merge branch 'master' into eric-wieser/free_algebra-grading

7c580605

github-actions removed merge-conflict

eric-wieser commented on 2020-12-04

bryangingechen removed awaiting-review

bryangingechen added awaiting-author

github-actions added merge-conflict

kim-em added too-late

Reviewers

bryangingechen

kbuzzard

rwbarton

Assignees

No one assigned

Labels

awaiting-author merge-conflict too-late

Milestone

No milestone

mathlib3 feat(algebra/free_algebra): Define a grading #4321 Open

feat(algebra/free_algebra): Define a grading #4321

mathlib3
feat(algebra/free_algebra): Define a grading
#4321

Open