-
Notifications
You must be signed in to change notification settings - Fork 234
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: a / c ≡ b / c [PMOD p]
#9619
Conversation
From LeanAPAP
@@ -321,6 +321,10 @@ theorem int_cast_modEq_int_cast {a b z : ℤ} : a ≡ b [PMOD (z : α)] ↔ a | |||
norm_cast | |||
#align add_comm_group.int_cast_modeq_int_cast AddCommGroup.int_cast_modEq_int_cast | |||
|
|||
@[simp, norm_cast] | |||
lemma intCast_modEq_intCast' {a b : ℤ} {n : ℕ} : a ≡ b [PMOD (n : α)] ↔ a ≡ b [PMOD (n : ℤ)] := by |
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.
Why intCast
, not int_cast
? The previous lemma uses int_cast
.
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.
It's one operation, so should be one atom. Let me fix the previous 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.
OTOH, we have Function.Involutive.list_map
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 don't think we should block this PR on a naming decision that mathlib isn't consistent about.
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
Pull request successfully merged into master. Build succeeded: |
a / c ≡ b / c [PMOD p]
a / c ≡ b / c [PMOD p]
Also fix a few misported names.
From LeanAPAP