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/fin): add_comm_monoid and simp lemmas #5010
Conversation
New lemmas: `add_zero` `zero_add` `mul_one` `one_mul`
I guess the question is, whether these lemmas should be available in |
New lemmas: `add_zero` `zero_add` `mul_one` `one_mul`
…-community/mathlib into fin-monoid-identities
I know there's some controversy about arithmetic operations on
This PR doesn't add to the controversy, and the simp lemmas clean up the situation slightly. (Although you could argue that cleaning things up encourages people to use the controversial operations...) I think it's fine to merge this until there's a better story about bors merge |
Provide `add_comm_monoid` for `fin (n + 1)`, which makes proofs that have to do with `bit0`, `bit1`, and `nat.cast` and related happy. Provide the specialized lemmas as simp lemmas. Also provide various simp lemmas about multiplication, but without the associated `comm_monoid`.
Pull request successfully merged into master. Build succeeded: |
Provide
add_comm_monoid
forfin (n + 1)
, which makes proofs that have to do withbit0
,bit1
, andnat.cast
and related happy. Provide the specialized lemmas as simp lemmas. Also provide various simp lemmas about multiplication, but without the associatedcomm_monoid
.I didn't make the
comm_monoid
for multiplication, partially because I don't have a direct need for it, and partially because I couldn't juggle themul_assoc
proof out of the modular arithmetic nor backport from thezmod
file.