-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(algebra): commuting elements #1089
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Some minor comments. I haven't read the long proofs yet.
Hi, |
Where are up to with this PR? (Neil, if you click the "resolve conversation" button as well as (or even instead of) saying "Done", it's easier for later reviewers to see the status. I've gone through and clicked resolve on a bunch.) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this is almost ready to go. Some minor changes suggested.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A few minor changes
@jcommelin @ChrisHughes24 I reordered theorems to avoid repeating ourselves, and added lemmas like |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
@robertylewis All the defs now have a docstring, as does the binomial theorem. All the other lemmas are trivialities. I don't think we should require all of those to have a docstring as well, do we?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
All the other lemmas are trivialities. I don't think we should require all of those to have a docstring as well, do we?
The guidelines we came up with say that all defs and "important" lemmas should have doc strings.
* Not sure how this works * Small refactor of geometric sums * Properties of commuting elements * Geometric sums moved to geom_sum.lean * Geometric sums, two commuting variables * Import geom_sum.lean * Cover commuting elements of noncommutative rings * Whitespace * Add file headers * Delete stray file * Sum/prod over range 0, range 1 * Add simp lemmas * Various changes from PR review * Add semigroup case * Changes from PR review * Corrected all_commute to commute.all * Minor changes from PR review * Change line endings back to unix * `@[to_additive]` can't be a `local attribute` * Rename `add_pow_comm` to `add_pow_of_commute` as suggested by @jcommelin * Add a few missing instances * DRY * Notation for `gsmul` should go into `add_group`, not `group` * Prove `gsmul_one` * Reorder `algebra/commute`, add more lemmas * Add docs, rename `geom_sum₂_mul_add_comm` to `commute.geom_sum₂_mul_add`. * Rename, add a docstring * Fix a typo spotted by @ChrisHughes24 * Move common args to `variables` * Rename `commute.mul` to `commute.mul_right` etc. * Add some `@[simp]` attributes. * More `@[simp]` * Add some `_iff` versions
(a * b) ^ n = a ^ n * b ^ n
to this context.a ^ n - b ^ n
whena
andb
commute. (Previously we only had this forb = 1
.) Refactor uses of theb = 1
case slightly.big_operators.lean
togeom_sum.lean
, to avoid issues with order of imports.Note: a few days ago I submitted a PR dealing with various properties of elements in commutative rings. It was suggested that some parts should be generalised to the noncommutative case. I closed that PR because of some git-related problems, but will resubmit it latter in smaller chunks. This PR is intended to support the requested generalisation.