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] - chore(algebra/group_ring_action): docstring, move monoid.End to algebra/group/hom #3671
Conversation
kckennylau
commented
Aug 3, 2020
•
edited
edited
# Group action on rings | ||
|
||
This file defines the typeclass of monoid acting on semirings `mul_semiring_action M R`, | ||
and the corresponding typeclass of invariant subrings. |
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.
Please mention that algebra
does not satisfy axioms of mul_semiring_action
.
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.
done
src/algebra/group/hom.lean
Outdated
one_mul := monoid_hom.id_comp } | ||
|
||
instance monoid.End.inhabited : inhabited (monoid.End M) := | ||
⟨1⟩ |
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.
Could you please define has_coe_to_fun
and add lemmas coe_one : ((1 : monoid.End M) : M → M) = id
and coe_mul : ((f * g : monoid.End M) : M → M) = f ∘ g
in monoid
and add_monoid
namespaces?
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.
done
bors merge |
Pull request successfully merged into master. Build succeeded: |