mathlib3
feat(algebra): commuting elements
#1089
Merged
Overview
Commits
41
Changes
View On GitHub

feat(algebra): commuting elements #1089

mergify merged 41 commits into leanprover-community:master from NeilStrickland:commute
NeilStrickland
NeilStrickland Not sure how this works
79401527
NeilStrickland Merge remote-tracking branch 'upstream/master'
3efbd6f6
NeilStrickland Small refactor of geometric sums
56843eff
NeilStrickland Properties of commuting elements
4dcd6108
NeilStrickland Geometric sums moved to geom_sum.lean
43b80d9e
NeilStrickland Geometric sums, two commuting variables
417abb2f
NeilStrickland Import geom_sum.lean
97c23e67
NeilStrickland Cover commuting elements of noncommutative rings
19b048da
NeilStrickland Whitespace
506fa2be
NeilStrickland NeilStrickland requested a review 6 years ago
NeilStrickland Add file headers
b0980efe
NeilStrickland Delete stray file
9800dbc9
jcommelin
jcommelin commented on 2019-05-28
NeilStrickland Sum/prod over range 0, range 1
0f0bb2ce
NeilStrickland Add simp lemmas
16f6ee13
NeilStrickland Various changes from PR review
2528f45c
NeilStrickland Add semigroup case
4570ce92
NeilStrickland Changes from PR review
d72c991b
NeilStrickland Corrected all_commute to commute.all
a1c0d574
urkud
urkud commented on 2019-06-04
urkud
urkud commented on 2019-06-04
urkud
jcommelin
jcommelin commented on 2019-06-10
NeilStrickland Minor changes from PR review
cc6d24ba
kim-em
jcommelin jcommelin assigned jcommelin jcommelin 6 years ago
jcommelin jcommelin assigned ChrisHughes24 ChrisHughes24 6 years ago
jcommelin
jcommelin dismissed these changes on 2019-07-09
ChrisHughes24
ChrisHughes24 requested changes on 2019-07-13
robertylewis robertylewis added needs-documentation
robertylewis
robertylewis robertylewis added awaiting-author
urkud Change line endings back to unix
8851365d
urkud Merge branch 'master' into commute
4fb835a3
urkud Merge branch 'master' into commute
ce5f2f33
urkud
urkud `@[to_additive]` can't be a `local attribute`
fb2c92ef
urkud Rename `add_pow_comm` to `add_pow_of_commute` as suggested by @jcommelin
82444fb9
rwbarton
rwbarton commented on 2019-09-27
urkud Add a few missing instances
03d97800
urkud DRY
442eb4f8
urkud Notation for `gsmul` should go into `add_group`, not `group`
c524f9d0
urkud Prove `gsmul_one`
5593c844
urkud Reorder `algebra/commute`, add more lemmas
c4e66304
urkud Merge branch 'master' into commute
b5426fce
urkud
urkud Merge branch 'master' into commute
5efcf49b
urkud Merge branch 'master' into commute
36f8fda4
jcommelin
jcommelin commented on 2019-10-01
robertylewis
robertylewis commented on 2019-10-01
urkud Add docs, rename `geom_sum₂_mul_add_comm` to `commute.geom_sum₂_mul_a…
789fe603
urkud Rename, add a docstring
3eac2d91
urkud Merge branch 'master' into commute
9f8d6536
urkud urkud removed needs-documentation
ChrisHughes24
ChrisHughes24 commented on 2019-10-02
urkud Fix a typo spotted by @ChrisHughes24
c499277a
urkud Move common args to `variables`
cbc640e9
urkud Rename `commute.mul` to `commute.mul_right` etc.
bb8d97ab
urkud Add some `@[simp]` attributes.
83b6c03f
urkud More `@[simp]`
b84ce25c
urkud Add some `_iff` versions
27309a33
ChrisHughes24
ChrisHughes24 approved these changes on 2019-10-04
ChrisHughes24 ChrisHughes24 added ready-to-merge
ChrisHughes24 ChrisHughes24 removed awaiting-author
ChrisHughes24 ChrisHughes24 dismissed their stale review 6 years ago
Changes made
mergify[bot] Merge branch 'master' into commute
aa95e33d
mergify mergify merged 494132e1 into master 6 years ago

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
Labels
ready-to-merge
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum