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
[Merged by Bors] - feat(data/finset/noncomm_prod): add noncomm_prod_mul_distrib #12524
Conversation
adding `list.prod_commute`, `multiset.noncomm_prod_commute` and `finset.noncomm_prod_commute`.
The non-commutative version of `finset.sum_union`
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This PR/issue depends on: |
src/data/finset/noncomm_prod.lean
Outdated
noncomm_prod s (f * g) | ||
begin | ||
intros x hx y hy, | ||
by_cases h : x = y, { subst h }, | ||
apply commute.mul_left; apply commute.mul_right, | ||
{ exact comm_ff x hx y hy }, | ||
{ exact (comm_gf y hy x hx (ne.symm h)).symm }, | ||
{ exact comm_gf x hx y hy h }, | ||
{ exact comm_gg x hx y hy }, | ||
end | ||
= noncomm_prod s f comm_ff * noncomm_prod s g comm_gg := |
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 the statement would become more readable if you extracted the subproof into a separate aux-lemma.
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.
Like this?
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.
Thanks 🎉
bors merge
The non-commutative version of `finset.sum_union`.
Pull request successfully merged into master. Build succeeded: |
The non-commutative version of `finset.sum_union`.
The non-commutative version of
finset.sum_union
.