feat(Data/Fin/Parity): add lemmas about parity of `Fin` numbers #8960

urkud · 2023-12-10T22:32:12Z

Co-authored-by: Iván Renison [email protected]

Motivated by this Zulip question.

depends on: [Merged by Bors] - feat(Data/Fin): add lemmas #8974

Mathlib/Data/Fin/Parity.lean

leanprover-community-mathlib4-bot · 2023-12-16T02:11:38Z

This PR/issue depends on:

~~[Merged by Bors] - feat(Data/Fin): add lemmas #8974~~
By Dependent Issues (🤖). Happy coding!

IvanRenison · 2024-11-01T14:54:18Z

@urkud are you going to continue with this pull request? If not, can I continue with it?

urkud · 2024-11-01T14:56:45Z

Feel free to take over this PR. Thanks!

Ruben-VandeVelde

maintainer merge

github-actions · 2024-11-06T21:24:47Z

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

kim-em · 2024-11-06T23:03:53Z

bors merge

Co-authored-by: Iván Renison <[email protected]> Co-authored-by: Iván Renison <[email protected]>

IvanRenison · 2024-11-06T23:23:48Z

For some reason the commit has the "Co-authored-by" two times

mathlib-bors · 2024-11-06T23:31:48Z

Build failed:

Build

bryangingechen · 2024-11-07T03:37:28Z

bors d=IvanRenison

mathlib-bors · 2024-11-07T03:37:31Z

✌️ IvanRenison can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bryangingechen · 2024-11-07T03:38:28Z

Please merge master, fix the breakage and then merge with bors d+ when done, thanks!

Command-Master · 2024-11-05T16:02:59Z

Mathlib/Algebra/Group/Nat.lean

@@ -141,6 +141,18 @@ lemma two_mul_div_two_of_even : Even n → 2 * (n / 2) = n := fun h ↦
 lemma div_two_mul_two_of_even : Even n → n / 2 * 2 = n :=
  fun h ↦ Nat.div_mul_cancel ((even_iff_exists_two_nsmul _).1 h)

+theorem one_lt_of_ne_zero_and_even {n : ℕ} (h0 : n ≠ 0) (hn : Even n) : 1 < n := by


According to the naming convention this should be one_lt_of_ne_zero_of_even.

Command-Master · 2024-11-05T16:04:07Z

Mathlib/Algebra/Group/Nat.lean

+  rw [h] at hn
+  exact Nat.not_even_one hn
+
+theorem add_one_lt_of_even_and_even_and_lt {n m : ℕ} (hn : Even n) (hm : Even m) (hnm : n < m) :


According to the naming convention this should be add_one_lt_of_even_of_even_of_lt, but in any case that's quite long - I think add_one_lt_of_even is clear enough

Command-Master · 2024-11-05T16:06:07Z

Mathlib/Data/Fin/Basic.lean

@@ -430,6 +430,13 @@ theorem val_add_eq_ite {n : ℕ} (a b : Fin n) :
    Nat.mod_eq_of_lt (show ↑b < n from b.2)]
 --- Porting note: syntactically the same as the above

+theorem val_add_eq_mod {n : ℕ} (a b : Fin n) : (a + b).val = (a.val + b.val) % n := rfl


This seems to be the same as Fin.val_add

Command-Master · 2024-11-05T16:07:43Z

Mathlib/Data/Fin/Basic.lean

@@ -430,6 +430,13 @@ theorem val_add_eq_ite {n : ℕ} (a b : Fin n) :
    Nat.mod_eq_of_lt (show ↑b < n from b.2)]
 --- Porting note: syntactically the same as the above

+theorem val_add_eq_mod {n : ℕ} (a b : Fin n) : (a + b).val = (a.val + b.val) % n := rfl
+
+theorem val_add_eq_of_sum_lt {n : ℕ} {a b : Fin n} (huv : a.val + b.val < n) :


According to the naming convention this should be val_add_eq_of_add_lt - sum is for sums of sets/lists/etc.

Command-Master · 2024-11-05T16:13:24Z

Mathlib/Data/Fin/Basic.lean

@@ -451,6 +458,8 @@ whose value is the original number. -/
 theorem val_cast_of_lt {n : ℕ} [NeZero n] {a : ℕ} (h : a < n) : (a : Fin n).val = a :=
  Nat.mod_eq_of_lt h

+theorem one_val_cast {n : ℕ} [NeZero n] (h : 1 < n) : (1 : Fin n).val = 1 := val_cast_of_lt h


What do you need this for? Can't you use val_cast_of_lt directly, or val_cast_of_lt (a := 1)?

Command-Master · 2024-11-07T10:25:48Z

Apologies for the late review, I forgot to send it earlier

urkud added 2 commits December 10, 2023 16:31

Snapshot

492278d

Fix

921892e

urkud added awaiting-review t-algebra Algebra (groups, rings, fields, etc) t-order Order theory labels Dec 10, 2023

Rename

5bae0d0

eric-wieser reviewed Dec 10, 2023

View reviewed changes

Mathlib/Data/Fin/Parity.lean Outdated Show resolved Hide resolved

Fix

c89b0d6

urkud added the awaiting-CI label Dec 10, 2023

eric-wieser reviewed Dec 10, 2023

View reviewed changes

Mathlib/Data/Fin/Parity.lean Outdated Show resolved Hide resolved

urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Dec 11, 2023

leanprover-community-mathlib4-bot added blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Dec 11, 2023

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 16, 2023

Merge branch 'master' into YK-fin-even

1c59c3f

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 20, 2023

github-actions bot removed the awaiting-CI label Dec 21, 2023

+2 lemmas

d8c187a

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Feb 8, 2024

urkud added 2 commits May 24, 2024 19:29

Merge master into YK-fin-even (using imerge)

fb6546f

Restore 2 lemmas

711bd9d

urkud added 5 commits May 31, 2024 01:38

Merge master into YK-fin-even (using imerge)

a98199b

Update

7cebff1

Move 2 lemmas

c07ca80

Merge master into YK-fin-even (using imerge)

c8c912c

Update

a788a98

Merge branch 'master' into YK-fin-even

20956ae

github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Nov 1, 2024

IvanRenison added 4 commits November 3, 2024 18:15

Partial progress

2fc8beb

Fix

0a359a5

More fixes

efd2d4a

Rename lemmas and add some new ones

57fcd27

IvanRenison changed the title ~~feat(Fin/Parity): add Fin.even_iff~~ feat(Data/Fin/Parity): add lemmas about parity of Fin numbers Nov 4, 2024

Add doc string for ' lemmas

c202c53

IvanRenison removed the awaiting-author A reviewer has asked the author a question or requested changes label Nov 4, 2024

Ruben-VandeVelde approved these changes Nov 6, 2024

View reviewed changes

github-actions bot added the maintainer-merge label Nov 6, 2024

github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 6, 2024

mathlib-bors bot pushed a commit that referenced this pull request Nov 6, 2024

feat(Data/Fin/Parity): add lemmas about parity of Fin numbers (#8960)

3930ac2

Co-authored-by: Iván Renison <[email protected]> Co-authored-by: Iván Renison <[email protected]>

bryangingechen added awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI and removed ready-to-merge This PR has been sent to bors. awaiting-author A reviewer has asked the author a question or requested changes labels Nov 7, 2024

github-actions bot added the delegated label Nov 7, 2024

Command-Master reviewed Nov 7, 2024

View reviewed changes

Command-Master added the awaiting-author A reviewer has asked the author a question or requested changes label Nov 7, 2024

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Data/Fin/Parity): add lemmas about parity of `Fin` numbers #8960

feat(Data/Fin/Parity): add lemmas about parity of `Fin` numbers #8960

urkud commented Dec 10, 2023 •

edited by IvanRenison

Loading

leanprover-community-mathlib4-bot commented Dec 16, 2023

IvanRenison commented Nov 1, 2024

urkud commented Nov 1, 2024

Ruben-VandeVelde left a comment

github-actions bot commented Nov 6, 2024

kim-em commented Nov 6, 2024

IvanRenison commented Nov 6, 2024

mathlib-bors bot commented Nov 6, 2024

bryangingechen commented Nov 7, 2024

mathlib-bors bot commented Nov 7, 2024

bryangingechen commented Nov 7, 2024

Command-Master Nov 5, 2024

Command-Master Nov 5, 2024

Command-Master Nov 5, 2024

Command-Master Nov 5, 2024

Command-Master Nov 5, 2024

Command-Master commented Nov 7, 2024

feat(Data/Fin/Parity): add lemmas about parity of Fin numbers #8960

Are you sure you want to change the base?

feat(Data/Fin/Parity): add lemmas about parity of Fin numbers #8960

Conversation

urkud commented Dec 10, 2023 • edited by IvanRenison Loading

leanprover-community-mathlib4-bot commented Dec 16, 2023

IvanRenison commented Nov 1, 2024

urkud commented Nov 1, 2024

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

github-actions bot commented Nov 6, 2024

kim-em commented Nov 6, 2024

IvanRenison commented Nov 6, 2024

mathlib-bors bot commented Nov 6, 2024

bryangingechen commented Nov 7, 2024

mathlib-bors bot commented Nov 7, 2024

bryangingechen commented Nov 7, 2024

Command-Master Nov 5, 2024

Choose a reason for hiding this comment

Command-Master Nov 5, 2024

Choose a reason for hiding this comment

Command-Master Nov 5, 2024

Choose a reason for hiding this comment

Command-Master Nov 5, 2024

Choose a reason for hiding this comment

Command-Master Nov 5, 2024

Choose a reason for hiding this comment

Command-Master commented Nov 7, 2024

feat(Data/Fin/Parity): add lemmas about parity of `Fin` numbers #8960

feat(Data/Fin/Parity): add lemmas about parity of `Fin` numbers #8960

urkud commented Dec 10, 2023 •

edited by IvanRenison

Loading