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: port Data.Fin.Basic #1084
Conversation
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.
There's a refactor hidden in the adhoc port here
This refactor was in the ad-hoc code, but is a distraction from the port, and isn't a clear win anyway.
Thanks 🎉 bors merge |
mathlib3 SHA: 0bd2ea37bcba5769e14866170f251c9bc64e35d7 Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Canceled. |
bors merge |
mathlib3 SHA: 0bd2ea37bcba5769e14866170f251c9bc64e35d7 Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
Pull request successfully merged into master. Build succeeded:
|
@[simp] | ||
theorem coe_ofNat_eq_mod' (m n : ℕ) [NeZero m] : | ||
(@Fin.ofNat' m n (Nat.pos_of_ne_zero (NeZero.ne m)) : ℕ) = n % m := | ||
rfl | ||
#align fin.coe_of_nat_eq_mod' Fin.coe_ofNat_eq_mod' | ||
|
||
@[simp] | ||
theorem coe_of_nat_eq_mod (m n : ℕ) : ((n : Fin (m+1)) : ℕ) = n % Nat.succ m := | ||
rfl | ||
#align fin.coe_of_nat_eq_mod Fin.coe_of_nat_eq_mod |
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.
seems we need a matching PR to #18131. @negiizhao will you do it?
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.
Just noticed the LHS of these two theorems look syntactically different, but they were the same in mathlib3. The latter is now removed from mathlib3, and the former is renamed to the latter, so the first #align should fail and the second #align should be a misalignment now. Can we change the statement of the former to ((n : Fin m) : ℕ) = n % m
and remove the latter?
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.
mathlib3 SHA: 0bd2ea37bcba5769e14866170f251c9bc64e35d7 Co-authored-by: Moritz Doll <moritz.doll@googlemail.com> Co-authored-by: Johan Commelin <johan@commelin.net>
mathlib3 SHA: 0bd2ea37bcba5769e14866170f251c9bc64e35d7