-
Notifications
You must be signed in to change notification settings - Fork 299
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(algebra/*,group_theory/*): instances/lemmas about is_scalar_tower
and smul_comm_class
#9533
Conversation
urkud
commented
Oct 4, 2021
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@[to_additive] | ||
instance smul_comm_class_both [monoid N] [monoid P] [has_scalar M N] [has_scalar M P] | ||
[smul_comm_class M N N] [smul_comm_class M P P] : | ||
smul_comm_class M (N × P) (N × P) := | ||
⟨λ c x y, by simp [smul_def, mul_def, mul_smul_comm]⟩ |
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.
Strictly we should also have the
@[to_additive] | |
instance smul_comm_class_both [monoid N] [monoid P] [has_scalar M N] [has_scalar M P] | |
[smul_comm_class M N N] [smul_comm_class M P P] : | |
smul_comm_class M (N × P) (N × P) := | |
⟨λ c x y, by simp [smul_def, mul_def, mul_smul_comm]⟩ | |
@[to_additive] | |
instance smul_comm_class_both' [monoid N] [monoid P] [has_scalar M N] [has_scalar M P] | |
[smul_comm_class N M N] [smul_comm_class P M P] : | |
smul_comm_class (N × P) M (N × P) := | |
sorry |
version
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 prefer to add instances as we need them.
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.
bors d+
Two nits, but feel free to merge as is if you don't care about them.
instance _root_.smul_comm_class.opposite_mid {M N} [monoid N] [has_scalar M N] | ||
[is_scalar_tower M N N] : | ||
smul_comm_class M Nᵒᵖ N := | ||
⟨λ x y z, by { induction y using opposite.op_induction, simp [smul_mul_assoc] }⟩ |
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 suspect this has a much shorter term mode proof, but not worth spending much time on.
lemma is_scalar_tower.of_smul_one_mul {M N} [monoid N] [has_scalar M N] | ||
(h : ∀ (x : M) (y : N), (x • (1 : N)) * y = x • y) : | ||
is_scalar_tower M N N := | ||
⟨λ x y z, by rw [← h, smul_eq_mul, mul_assoc, h, smul_eq_mul]⟩ |
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.
If we had a is_scalar_tower.of_smul_mul_assoc
then this proof probably becomes shorter.
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
…er` and `smul_comm_class` (#9533) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Build failed (retrying...): |
…er` and `smul_comm_class` (#9533) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
is_scalar_tower
and smul_comm_class
is_scalar_tower
and smul_comm_class