[Merged by Bors] - feat(Algebra/Group/Even): Add missing lemmas by artie2000 · Pull Request #20818 · leanprover-community/mathlib4

artie2000 · 2025-01-18T03:20:13Z

Make API for IsSquare / Even consistent between the "official" definition and equivalent ones
Add new lemma exists_apply_eq_and_isSquare that's analogous to IsSquare.map

depends on: [Merged by Bors] - chore(Algebra/Group/Even): Clean up file #20558

mergify · 2025-01-18T03:20:48Z

⚠️ The sha of the head commit of this PR conflicts with #20558. Mergify cannot evaluate rules on this PR. ⚠️

github-actions · 2025-01-18T03:21:05Z

PR summary 658f45e58d

Import changes exceeding 2%

%	File
+4.02%	`Mathlib.Algebra.Group.Even`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Group.Even	224	233	+9 (+4.02%)

Import changes for all files

Files	Import difference
`Mathlib.Data.Int.Bitwise` `Mathlib.Data.Nat.Bitwise`	2
8 files `Mathlib.Algebra.Group.Int.Even` `Mathlib.Algebra.Group.NatPowAssoc` `Mathlib.Algebra.Ring.Associator` `Mathlib.Data.Nat.Cast.Basic` `Mathlib.Data.Nat.Cast.Field` `Mathlib.Tactic.Abel` `Mathlib.Tactic.NoncommRing` `Mathlib.Tactic.NormNum.Basic`	6
3 files `Mathlib.Algebra.Group.Even` `Mathlib.Algebra.Group.Irreducible.Lemmas` `Mathlib.Algebra.Group.Nat.Even`	9

Declarations diff

+ isSquare_iff_exists_mul_self
+ isSquare_subset_image_isSquare
+ ⟨IsSquare.exists_mul_self,

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

mergify · 2025-01-18T22:35:25Z

⚠️ The sha of the head commit of this PR conflicts with #20558. Mergify cannot evaluate rules on this PR. ⚠️

mergify · 2025-01-21T02:23:19Z

⚠️ The sha of the head commit of this PR conflicts with #20558. Mergify cannot evaluate rules on this PR. ⚠️

Mathlib/Algebra/Group/Even.lean

Mathlib/Data/Set/Operations.lean

leanprover-community-bot-assistant · 2025-05-25T13:19:38Z

This pull request has conflicts, please merge master and resolve them.

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2025-06-10T16:38:48Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

Vierkantor · 2025-06-11T09:03:48Z

Mathlib/Data/Set/Basic.lean

-theorem setOf_set {s : Set α} : setOf s = s :=
-  rfl
-
-theorem setOf_app_iff {p : α → Prop} {x : α} : { x | p x } x ↔ p x :=
-  Iff.rfl
-
-theorem mem_def {a : α} {s : Set α} : a ∈ s ↔ s a :=
-  Iff.rfl


These got lost during this PR. From the commit history, looks like it's intentional. (And I agree we don't want them.) Could you update the description to reflect the changes?

They are being deleted in #25669

Aha! So let's wait for that one to be merged first.

I detangled them, do you still want me to hold off?

Vierkantor

It's slightly frustrating that the lightweight definitions file Data.Set.Operations is growing again, but that's not something to solve in this PR. And the consequences are relatively limited. So in all, I'm okay with merging this.

bors d+

mathlib-bors · 2025-06-11T09:05:00Z

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

artie2000 · 2025-06-11T10:25:22Z

@Vierkantor yes, although the other operations in Data.Set.Operations have their projections defined there, whereas setOf had its projections defined in the file Data.Set.Basic file (requiring lots of order theory), so I'd argue it's a principled move

commit 9e89453 Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 17:07:56 2025 +0100 remove defeq abuse commit fb45356 Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 17:03:43 2025 +0100 alias commit 9fd0c91 Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 16:56:16 2025 +0100 clean diff commit c12a864 Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 16:54:58 2025 +0100 style commit 99f3e36 Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 16:53:28 2025 +0100 style commit 5ab909f Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 16:47:21 2025 +0100 style commit 251e6cb Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 16:45:49 2025 +0100 revert things commit 31eeede Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 11:41:41 2025 +0100 move more stuff back commit 7a276bf Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 10:37:03 2025 +0100 nicer notation commit 8a46516 Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 10:33:10 2025 +0100 fix update commit 9fc0b3c Merge: 2a9c27c e99fde2 Author: artie2000 <artem.khovanov@gmail.com> Date: Tue Jun 10 10:32:57 2025 +0100 Merge branch 'master' into artie2000-even-new-theorems commit 2a9c27c Author: artie2000 <artem.khovanov@gmail.com> Date: Mon Jan 27 18:03:02 2025 +0000 move set lemmas earlier commit a0cc75b Author: artie2000 <artem.khovanov@gmail.com> Date: Thu Jan 23 14:43:17 2025 +0000 change proof commit 290c31e Author: Artie Khovanov <artem.khovanov@gmail.com> Date: Thu Jan 23 14:16:00 2025 +0000 Update Mathlib/Algebra/Group/Even.lean Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> commit a938bf1 Author: Artie Khovanov <artem.khovanov@gmail.com> Date: Thu Jan 23 14:09:54 2025 +0000 Update Mathlib/Algebra/Group/Even.lean Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> commit 1311f65 Merge: 8084f8b da8db71 Author: artie2000 <artem.khovanov@gmail.com> Date: Thu Jan 23 13:25:42 2025 +0000 Merge branch 'master' into artie2000-even-new-theorems commit 8084f8b Author: artie2000 <artem.khovanov@gmail.com> Date: Thu Jan 23 13:25:04 2025 +0000 fix sync commit 66e7e34 Author: artie2000 <artem.khovanov@gmail.com> Date: Thu Jan 23 13:22:23 2025 +0000 sync commit 42e8bcd Author: Artie Khovanov <artem.khovanov@gmail.com> Date: Tue Jan 21 11:10:02 2025 +0000 fix style commit 5ece3c4 Merge: 39ed89a a4c5ecf Author: artie2000 <artem.khovanov@gmail.com> Date: Sat Jan 18 03:06:23 2025 +0000 Merge branch 'master' into artie2000-automate-even commit 39ed89a Author: Artie Khovanov <artem.khovanov@gmail.com> Date: Wed Jan 15 22:42:29 2025 +0000 improve some proofs commit ee1b421 Author: Artie Khovanov <artem.khovanov@gmail.com> Date: Wed Jan 15 20:37:05 2025 +0000 style commit 31e725b Author: Artie Khovanov <artem.khovanov@gmail.com> Date: Wed Jan 15 20:34:37 2025 +0000 fix commit c15efe4 Author: artie2000 <artem.khovanov@gmail.com> Date: Wed Jan 15 20:20:46 2025 +0000 revert aesop commit 4d91399 Author: FM22 <artem.khovanov@gmail.com> Date: Mon Jan 13 03:32:19 2025 +0000 fix aesop probabilities commit 2fe6246 Author: FM22 <artem.khovanov@gmail.com> Date: Thu Jan 9 15:16:54 2025 +0000 fix commit 9d5d902 Author: FM22 <artem.khovanov@gmail.com> Date: Tue Jan 7 23:12:27 2025 +0000 rename variables for consistency commit d17a26d Author: FM22 <artem.khovanov@gmail.com> Date: Tue Jan 7 23:04:09 2025 +0000 move deprecations back commit 23a8966 Author: FM22 <artem.khovanov@gmail.com> Date: Tue Jan 7 23:01:53 2025 +0000 update name commit 77eff5d Author: FM22 <artem.khovanov@gmail.com> Date: Tue Jan 7 23:01:42 2025 +0000 fix commit 4686df9 Author: FM22 <artem.khovanov@gmail.com> Date: Tue Jan 7 22:13:41 2025 +0000 new lemma commit 09c31d4 Author: FM22 <artem.khovanov@gmail.com> Date: Tue Jan 7 21:35:00 2025 +0000 add example commit 76f7fa2 Author: FM22 <artem.khovanov@gmail.com> Date: Tue Jan 7 21:09:51 2025 +0000 initial commit

artie2000 · 2025-06-11T16:58:45Z

I have found that the changes to Data.Set.Operations are not necessary for this particular lemma about even elements. Apologies for time wasted. I will split the PRs and re-request a review.

mathlib4-dependent-issues-bot · 2025-06-11T18:07:25Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Algebra/Group/Even): Clean up file #20558~~
By Dependent Issues (🤖). Happy coding!

YaelDillies

Thanks!

maintainer merge

github-actions · 2025-06-11T18:31:50Z

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

jcommelin

Thanks 🎉

bors merge

* Make API for `IsSquare` / `Even` consistent between the "official" definition and equivalent ones * Add new lemma `exists_apply_eq_and_isSquare` that's analogous to `IsSquare.map`

mathlib-bors · 2025-06-12T06:02:18Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* master: (447 commits) chore(Data/Set): move very basic lemmas earlier (leanprover-community#25707) feat: preserve draft status when migrating PRs to fork (leanprover-community#25777) chore(Data/Set/Basic): deprecate lemmas that abuse the `Set α := α → Prop` defeq (leanprover-community#25669) refactor: redefine `ProperCone` as an `abbrev` for `ClosedSubmodule` (leanprover-community#25204) feat: interaction between ContinuousLinearMap.coprod and ContinuousLinearEquiv.prodComm (leanprover-community#25564) fix: outdated docstring (leanprover-community#25717) feat(MeasureTheory): convolution of measures with densities (leanprover-community#25718) feat: make sure that the simp normal form of equiv-like classes pushes `symm` and `trans` to the right (leanprover-community#25604) feat(ModelTheory): Formula.iSup and iInf (leanprover-community#21948) feat(RingTheory/Polynomial/ContentIdeal): the content ideal of a polynomial. (leanprover-community#25333) fix: typo in labels_from_comment.yml (leanprover-community#25727) feat: is{Inducing,Embedding}_prodMkLeft (leanprover-community#25705) feat: check that the mathlib options exist (leanprover-community#25687) feat(Algebra/Group/Even): Add missing lemmas (leanprover-community#20818) refactor: make `Matrix.kroneckerTMulAlgEquiv` heterogeneous (leanprover-community#25693) feat: allow contributors to remove labels with comments (leanprover-community#25723) chore: disable build.yml and bors.yml on forks (leanprover-community#25722) feat: improvements to user_activity_report.py (leanprover-community#25721) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) chore: update the migration script to check for necessary permissions and prefer ssh if possible (leanprover-community#25701) ...

) * Make API for `IsSquare` / `Even` consistent between the "official" definition and equivalent ones * Add new lemma `exists_apply_eq_and_isSquare` that's analogous to `IsSquare.map`

artie2000 requested a review from YaelDillies January 18, 2025 03:20

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 18, 2025

This was referenced Jan 18, 2025

[Merged by Bors] - chore(Algebra/Group/Even): Clean up file #20558

Closed

feat(Algebra): Add Aesop automation around Even / IsSquare. #20781

Closed

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 23, 2025

YaelDillies reviewed Jan 23, 2025

View reviewed changes

Mathlib/Algebra/Group/Even.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Group/Even.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Group/Even.lean Show resolved Hide resolved

Mathlib/Algebra/Group/Even.lean Outdated Show resolved Hide resolved

YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes. t-algebra Algebra (groups, rings, fields, etc) labels Jan 23, 2025

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 27, 2025

alreadydone reviewed Jan 29, 2025

View reviewed changes

Mathlib/Algebra/Group/Even.lean Outdated Show resolved Hide resolved

alreadydone reviewed Jan 29, 2025

View reviewed changes

Mathlib/Data/Set/Operations.lean Outdated Show resolved Hide resolved

leanprover-community-bot-assistant 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 25, 2025

github-actions 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 Jun 10, 2025

artie2000 requested a review from YaelDillies June 10, 2025 10:27

artie2000 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jun 10, 2025

YaelDillies approved these changes Jun 10, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 10, 2025

Vierkantor reviewed Jun 11, 2025

View reviewed changes

Vierkantor approved these changes Jun 11, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jun 11, 2025

artie2000 force-pushed the artie2000-even-new-theorems branch from 9e89453 to 7bb08ea Compare June 11, 2025 10:33

artie2000 force-pushed the artie2000-even-new-theorems branch from 7bb08ea to 75d6231 Compare June 11, 2025 10:43

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 11, 2025

artie2000 added 2 commits June 11, 2025 12:30

fix liniter

39244d6

update + shake

471fc9d

artie2000 added 2 commits June 11, 2025 18:08

split PR

0239519

fix ?

5ad18b0

artie2000 requested a review from YaelDillies June 11, 2025 17:16

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 11, 2025

YaelDillies approved these changes Jun 11, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jun 11, 2025

shake fix

325e4f9

jcommelin reviewed Jun 12, 2025

View reviewed changes

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jun 12, 2025

mathlib-bors bot changed the title ~~feat(Algebra/Group/Even): Add missing lemmas~~ [Merged by Bors] - feat(Algebra/Group/Even): Add missing lemmas Jun 12, 2025

mathlib-bors bot closed this Jun 12, 2025

mathlib-bors bot deleted the artie2000-even-new-theorems branch June 12, 2025 06:02

Conversation

artie2000 commented Jan 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mergify bot commented Jan 18, 2025

Uh oh!

github-actions bot commented Jan 18, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 658f45e58d

Import changes for modified files

Declarations diff

Uh oh!

mergify bot commented Jan 18, 2025

Uh oh!

mergify bot commented Jan 21, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

leanprover-community-bot-assistant commented May 25, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jun 10, 2025

Uh oh!

Vierkantor Jun 11, 2025

Choose a reason for hiding this comment

Uh oh!

YaelDillies Jun 11, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor Jun 11, 2025

Choose a reason for hiding this comment

Uh oh!

artie2000 Jun 11, 2025

Choose a reason for hiding this comment

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jun 11, 2025

Uh oh!

artie2000 commented Jun 11, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

artie2000 commented Jun 11, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Jun 11, 2025

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jun 11, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jun 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

artie2000 commented Jan 18, 2025 •

edited

Loading

github-actions bot commented Jan 18, 2025 •

edited

Loading

artie2000 commented Jun 11, 2025 •

edited

Loading