[Merged by Bors] - move(Algebra/Parity): Split file by YaelDillies · Pull Request #12829 · leanprover-community/mathlib4

YaelDillies · 2024-05-11T21:56:37Z

Parity of elements in a group/ring is a basic algebraic concept, but it currently requires importing a bunch of algebraic order theory. As a consequence, Algebra.Parity currently holds a bunch of lemmas that really belong in earlier files but cannot due to import cycles.

This PR moves the content of Algebra.Parity to

Algebra.Group.Even for the definition of IsSquare and Even
Algebra.Ring.Parity for the definition of Odd and ring properties of Even
Algebra.Order.Group.Abs, Algebra.Order.Ring.Abs, Algebra.Order.Ring.Canonical, Algebra.Order.Sub.Canonical, Algebra.GroupPower.Order for the various algebraic order properties of Even and Odd

As a result, Even/Odd are available much more widely without awkward dependencies and algebraic order lemmas are now in the correct files. The only slight downfall is that two lemmas in Algebra.Ring.Parity are stated using Set.range, hence I had to weaken a few assert_not_exists to forbidding Data.Set.Basic instead of Data.Set.Defs. This is inconsequential.

A side-effect of this PR is that I had to move some bit0/bit1 lemmas. I could not find anywhere sensible to put them, so I am currently keeping them in Algebra.Parity. As a result, I had to reprove a few lemmas in Algebra.GroupPower.Order. I took the opportunity to generalise them.

This is a followup to leanprover-community/mathlib3#17391 motivated by https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2EAlgebra.2EAssociated and the move-only part of #11863.

Parity of elements in a group/ring is a basic algebraic concept, but it currently requires importing a bunch of algebraic order theory. As a consequence, `Algebra.Parity` currently holds a bunch of lemmas that really belong in earlier files but cannot due to import cycles. This PR moves the content of `Algebra.Parity` to * `Algebra.Group.Even` for the definition of `IsSquare` and `Even` * `Algebra.Ring.Parity` for the definition of `Odd` and ring properties of `Even` * `Algebra.Order.Group.Abs`, `Algebra.Order.Ring.Abs`, `Algebra.Order.Ring.Canonical`, `Algebra.Order.Sub.Canonical`, `Algebra.GroupPower.Order` for the various algebraic order properties of `Even` and `Odd` As a result, `Even`/`Odd` are available much more widely without awkward dependencies and algebraic order lemmas are now in the correct files. The only slight downfall is that two lemmas in `Algebra.Ring.Parity` are stated using `Set.range`, hence I had to weaken a few `assert_not_exists` to forbidding `Data.Set.Basic` instead of `Data.Set.Defs`. This is inconsequential. A side-effect of this PR is that I had to move some `bit0`/`bit1` lemmas. I could not find anywhere sensible to put them, so I am currently keeping them in `Algebra.Parity`. As a result, I had to reprove a few lemmas in `Algebra.GroupPower.Order`. I took the opportunity to generalise them. This is a followup to leanprover-community/mathlib3#17391 motivated by https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2EAlgebra.2EAssociated and the move-only part of #11863.

adomani · 2024-05-12T09:11:55Z

Yaël, thank you for the new PR, as this gives me a way of testing some improvements to the no_lost_declarations script!

This is a summary of just the names that have changed in this PR:

+ Additive.instDecidablePredEven
- even_abs
+ isSquare_mabs
+ Multiplicative.instDecidablePredIsSquare

Does this seem a reasonable output?

YaelDillies · 2024-05-12T09:55:10Z

- even_abs is incorrect as isSquare_mabs gets additivised to even_abs. I guess your script doesn't know about to_additive?

adomani · 2024-05-12T10:26:41Z

The script is just text-based and it is supposed to be a quick check that does not require CI to have run. So, I think that it is fair if it flags as missing a to_additivized lemma.

The main idea is to help focus from the +474-478 lines to just checking the 4 highlighted lemmas.

This seems like a good simplification for reviewers.

YaelDillies · 2024-05-12T11:35:38Z

Yeah, makes sense. The rest of the list looks good.

adomani · 2024-05-12T11:48:53Z

Ok, thanks for confirming. I will make the very short diff available as an option, then.

github-actions · 2024-05-13T11:37:39Z

+ Additive.instDecidablePredEven
+ Multiplicative.instDecidablePredIsSquare
+ isSquare_mabs
- even_abs
-``- [DecidablePred

Ruben-VandeVelde

Thanks!

maintainer merge

github-actions · 2024-05-13T11:43:54Z

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

sgouezel · 2024-05-13T11:48:24Z

bors r+

YaelDillies · 2024-05-13T11:51:26Z

+ Additive.instDecidablePredEven

+ Multiplicative.instDecidablePredIsSquare

+ isSquare_mabs

- even_abs

-``- [DecidablePred

@adomani, there seems to be a formatting issue

adomani · 2024-05-13T11:54:20Z

Thanks for the report!

I can remove the extra `` easily. I would have to think about omitting the [inst], though, since this is one place where there is no name after instance and then it is unclear what should be used for comparison.

adomani · 2024-05-13T12:05:06Z

#12866

mathlib-bors · 2024-05-13T13:18:45Z

Merge conflict.

Fixes a formatting issue in the output of `move-decls`. As reported in #12829. On that PR, the new script reports *** * `+` Additive.instDecidablePredEven * `--` [DecidablePred * `-` even_abs * `+` isSquare_mabs * `+` Multiplicative.instDecidablePredIsSquare

jcommelin · 2024-05-15T09:42:44Z

bors r+

Parity of elements in a group/ring is a basic algebraic concept, but it currently requires importing a bunch of algebraic order theory. As a consequence, `Algebra.Parity` currently holds a bunch of lemmas that really belong in earlier files but cannot due to import cycles. This PR moves the content of `Algebra.Parity` to * `Algebra.Group.Even` for the definition of `IsSquare` and `Even` * `Algebra.Ring.Parity` for the definition of `Odd` and ring properties of `Even` * `Algebra.Order.Group.Abs`, `Algebra.Order.Ring.Abs`, `Algebra.Order.Ring.Canonical`, `Algebra.Order.Sub.Canonical`, `Algebra.GroupPower.Order` for the various algebraic order properties of `Even` and `Odd` As a result, `Even`/`Odd` are available much more widely without awkward dependencies and algebraic order lemmas are now in the correct files. The only slight downfall is that two lemmas in `Algebra.Ring.Parity` are stated using `Set.range`, hence I had to weaken a few `assert_not_exists` to forbidding `Data.Set.Basic` instead of `Data.Set.Defs`. This is inconsequential. A side-effect of this PR is that I had to move some `bit0`/`bit1` lemmas. I could not find anywhere sensible to put them, so I am currently keeping them in `Algebra.Parity`. As a result, I had to reprove a few lemmas in `Algebra.GroupPower.Order`. I took the opportunity to generalise them. This is a followup to leanprover-community/mathlib3#17391 motivated by https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2EAlgebra.2EAssociated and the move-only part of #11863.

mathlib-bors · 2024-05-15T10:47:42Z

Pull request successfully merged into master.

Build succeeded:

Fixes a formatting issue in the output of `move-decls`. As reported in #12829. On that PR, the new script reports *** * `+` Additive.instDecidablePredEven * `--` [DecidablePred * `-` even_abs * `+` isSquare_mabs * `+` Multiplicative.instDecidablePredIsSquare

Parity of elements in a group/ring is a basic algebraic concept, but it currently requires importing a bunch of algebraic order theory. As a consequence, `Algebra.Parity` currently holds a bunch of lemmas that really belong in earlier files but cannot due to import cycles. This PR moves the content of `Algebra.Parity` to * `Algebra.Group.Even` for the definition of `IsSquare` and `Even` * `Algebra.Ring.Parity` for the definition of `Odd` and ring properties of `Even` * `Algebra.Order.Group.Abs`, `Algebra.Order.Ring.Abs`, `Algebra.Order.Ring.Canonical`, `Algebra.Order.Sub.Canonical`, `Algebra.GroupPower.Order` for the various algebraic order properties of `Even` and `Odd` As a result, `Even`/`Odd` are available much more widely without awkward dependencies and algebraic order lemmas are now in the correct files. The only slight downfall is that two lemmas in `Algebra.Ring.Parity` are stated using `Set.range`, hence I had to weaken a few `assert_not_exists` to forbidding `Data.Set.Basic` instead of `Data.Set.Defs`. This is inconsequential. A side-effect of this PR is that I had to move some `bit0`/`bit1` lemmas. I could not find anywhere sensible to put them, so I am currently keeping them in `Algebra.Parity`. As a result, I had to reprove a few lemmas in `Algebra.GroupPower.Order`. I took the opportunity to generalise them. This is a followup to leanprover-community/mathlib3#17391 motivated by https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2EAlgebra.2EAssociated and the move-only part of #11863.

Fixes a formatting issue in the output of `move-decls`. As reported in #12829. On that PR, the new script reports *** * `+` Additive.instDecidablePredEven * `--` [DecidablePred * `-` even_abs * `+` isSquare_mabs * `+` Multiplicative.instDecidablePredIsSquare

Parity of elements in a group/ring is a basic algebraic concept, but it currently requires importing a bunch of algebraic order theory. As a consequence, `Algebra.Parity` currently holds a bunch of lemmas that really belong in earlier files but cannot due to import cycles. This PR moves the content of `Algebra.Parity` to * `Algebra.Group.Even` for the definition of `IsSquare` and `Even` * `Algebra.Ring.Parity` for the definition of `Odd` and ring properties of `Even` * `Algebra.Order.Group.Abs`, `Algebra.Order.Ring.Abs`, `Algebra.Order.Ring.Canonical`, `Algebra.Order.Sub.Canonical`, `Algebra.GroupPower.Order` for the various algebraic order properties of `Even` and `Odd` As a result, `Even`/`Odd` are available much more widely without awkward dependencies and algebraic order lemmas are now in the correct files. The only slight downfall is that two lemmas in `Algebra.Ring.Parity` are stated using `Set.range`, hence I had to weaken a few `assert_not_exists` to forbidding `Data.Set.Basic` instead of `Data.Set.Defs`. This is inconsequential. A side-effect of this PR is that I had to move some `bit0`/`bit1` lemmas. I could not find anywhere sensible to put them, so I am currently keeping them in `Algebra.Parity`. As a result, I had to reprove a few lemmas in `Algebra.GroupPower.Order`. I took the opportunity to generalise them. This is a followup to leanprover-community/mathlib3#17391 motivated by https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathlib.2EAlgebra.2EAssociated and the move-only part of #11863.

#12829 made `Algebra.Parity` almost empty. This PR deletes it.

YaelDillies added 2 commits May 11, 2024 21:56

update Mathlib

4e7d00d

YaelDillies added awaiting-review t-algebra Algebra (groups, rings, fields, etc) labels May 11, 2024

YaelDillies mentioned this pull request May 11, 2024

[Merged by Bors] - chore: Delete Algebra.Parity #11863

Closed

2 tasks

leanprover-community deleted a comment from github-actions bot May 11, 2024

fix

efeccfc

shake

700bd9d

YaelDillies requested a review from jcommelin May 12, 2024 11:36

Merge remote-tracking branch 'origin/master' into move_algebra_parity

8d8f67c

Ruben-VandeVelde added the move-decls label May 13, 2024

Ruben-VandeVelde approved these changes May 13, 2024

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label May 13, 2024

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 13, 2024

adomani mentioned this pull request May 13, 2024

[Merged by Bors] - fix: remove consecutive backticks #12866

Closed

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 13, 2024

Merge remote-tracking branch 'origin/master' into move_algebra_parity

26d5706

fix Algebra.Field.Power

d0c1578

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 15, 2024

mathlib-bors bot changed the title ~~move(Algebra/Parity): Split file~~ [Merged by Bors] - move(Algebra/Parity): Split file May 15, 2024

mathlib-bors bot closed this May 15, 2024

mathlib-bors bot deleted the move_algebra_parity branch May 15, 2024 10:47

YaelDillies mentioned this pull request May 15, 2024

[Merged by Bors] - chore: Delete Data.Nat.Parity #12882

Closed

1 task

mathlib-bors bot pushed a commit that referenced this pull request May 22, 2024

chore: Delete Algebra.Parity (#11863)

e7603ff

#12829 made `Algebra.Parity` almost empty. This PR deletes it.

callesonne pushed a commit that referenced this pull request Jun 4, 2024

chore: Delete Algebra.Parity (#11863)

b91cc6c

#12829 made `Algebra.Parity` almost empty. This PR deletes it.

js2357 pushed a commit that referenced this pull request Jun 18, 2024

chore: Delete Algebra.Parity (#11863)

affeef9

#12829 made `Algebra.Parity` almost empty. This PR deletes it.

Conversation

YaelDillies commented May 11, 2024

Uh oh!

adomani commented May 12, 2024

Uh oh!

YaelDillies commented May 12, 2024

Uh oh!

adomani commented May 12, 2024

Uh oh!

YaelDillies commented May 12, 2024

Uh oh!

adomani commented May 12, 2024

Uh oh!

github-actions bot commented May 13, 2024

Uh oh!

Ruben-VandeVelde left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented May 13, 2024

Uh oh!

sgouezel commented May 13, 2024

Uh oh!

YaelDillies commented May 13, 2024

Uh oh!

adomani commented May 13, 2024

Uh oh!

adomani commented May 13, 2024

Uh oh!

mathlib-bors bot commented May 13, 2024

Uh oh!

jcommelin commented May 15, 2024

Uh oh!

mathlib-bors bot commented May 15, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants