[Merged by Bors] - chore(Algebra/Group/Even): Clean up file by artie2000 · Pull Request #20558 · leanprover-community/mathlib4

artie2000 · 2025-01-07T21:11:14Z

Rename some theorems to remove primed variants
Move simp attribute from IsSquare.sq to Even.isSquare_pow for consistency
Remove unhelpful alias
Golf some proofs
Make notation consistent throughout proofs

Moves:
Even.nsmul -> Even.nsmul_right
Even.nsmul' -> Even.nsmul_left
Even.zsmul -> Even.zsmul_right
Even.zsmul' -> Even.zsmul_left
isSquare_zero -> IsSquare.zero

Deletions:
isSquare_of_exists_sq (prefer IsSquare.sq)

github-actions · 2025-01-07T21:12:05Z

PR summary b5a3e9dde1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Even.nsmul
+ Even.nsmul'
+ Even.zsmul
+ Even.zsmul'
+ IsSquare.zero
+ even_zero
+ ⟨_,
- IsSquare.inv
- isSquare_of_exists_sq

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).

Mathlib/Algebra/Group/Even.lean

YaelDillies

Sorry to be this person once again, but tweaking aesop priorities is so experimental that I would rather it be a standalone PR. Can you make it a separate PR depending on this one?

artie2000 · 2025-01-13T15:47:38Z

To clarify, no aesop attributes are changed here -- only added. One simp lemma is removed due to having an inappropriate form. Would you like me to move my additions of aesop attributes to a separate PR?

artie2000 · 2025-01-16T02:11:33Z

I'm not sure it's right to call this chore
I did add some new (easy) lemmas

YaelDillies · 2025-01-16T13:03:58Z

If none of feat, refactor, chore fits for all of a PR, then that probably means it should be split up into its feat, refactor, chore parts.

Mathlib/Algebra/Field/Power.lean

Mathlib/Algebra/Group/Nat/Even.lean

Mathlib/Algebra/Order/Field/Power.lean

Mathlib/Data/Bool/Count.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

YaelDillies

Thanks! 🚀

maintainer merge

github-actions · 2025-01-23T08:23:33Z

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

riccardobrasca · 2025-01-23T08:38:28Z

This PR is marked "awaiting author". Should the label be removed?

adomani

Thanks, this looks good!

Please, update the comment, if you want, add a sentence to the doc-string and then merge!

bors d+

Mathlib/Algebra/Group/Even.lean

adomani · 2025-01-23T08:41:53Z

Mathlib/Algebra/Group/Even.lean

 def IsSquare (a : α) : Prop := ∃ r, a = r * r

-@[to_additive (attr := simp)] lemma IsSquare.mul_self (m : α) : IsSquare (m * m) := ⟨m, rfl⟩
+@[to_additive (attr := simp)] lemma IsSquare.mul_self (r : α) : IsSquare (r * r) := ⟨r, rfl⟩


It looks like the undocumented convention is that r is a "square root" of a, where possible.

I don't think that it is too important to enforce this, but you can, if you want, add a sentence to the doc-string.

mathlib-bors · 2025-01-23T08:42:33Z

✌️ 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.

adomani · 2025-01-23T08:43:16Z

This PR is marked "awaiting author". Should the label be removed?

Ah, I had missed that!

bors d-

Co-authored-by: damiano <adomani@gmail.com>

…er-community/mathlib4 into artie2000-automate-even

artie2000 · 2025-01-23T11:01:36Z

@adomani I'm confused about the status of this PR. Should I go ahead with the merge?

YaelDillies · 2025-01-23T11:05:27Z

I think the confusion is simply that you forgot to remove awaiting-author. I would say you can merge, yes.

artie2000 · 2025-01-23T11:08:07Z

Oh sorry! I'll merge once it passes CI

artie2000 · 2025-01-23T11:42:31Z

bors r+

* Rename some theorems to remove primed variants * Move `simp` attribute from `IsSquare.sq` to `Even.isSquare_pow` for consistency * Remove unhelpful alias * Golf some proofs * Make notation consistent throughout proofs Moves: `Even.nsmul` -> `Even.nsmul_right` `Even.nsmul'` -> `Even.nsmul_left` `Even.zsmul` -> `Even.zsmul_right` `Even.zsmul'` -> `Even.zsmul_left` `isSquare_zero` -> `IsSquare.zero` Deletions: `isSquare_of_exists_sq` (prefer `IsSquare.sq`)

mathlib-bors · 2025-01-23T12:19:52Z

Pull request successfully merged into master.

Build succeeded:

adomani · 2025-01-23T14:31:54Z

Yes, I had overlooked the awaiting-author label, but I was happy with the form that the PR had anyway!

initial commit

76f7fa2

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 7, 2025

artie2000 requested a review from YaelDillies January 7, 2025 21:33

artie2000 added 5 commits January 7, 2025 21:35

add example

09c31d4

new lemma

4686df9

fix

77eff5d

update name

23a8966

move deprecations back

d17a26d

artie2000 marked this pull request as ready for review January 7, 2025 23:08

rename variables for consistency

9d5d902

YaelDillies reviewed Jan 8, 2025

View reviewed changes

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

artie2000 marked this pull request as draft January 8, 2025 19:57

fix

2fe6246

artie2000 marked this pull request as ready for review January 13, 2025 03:18

fix aesop probabilities

4d91399

YaelDillies reviewed Jan 13, 2025

View reviewed changes

artie2000 mentioned this pull request Jan 15, 2025

[Merged by Bors] - feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings #16094

Closed

7 tasks

artie2000 added 3 commits January 15, 2025 20:20

revert aesop

c15efe4

fix

31e725b

style

ee1b421

artie2000 changed the title ~~feat(Algebra/Group/Even): Clean up file, add Aesop automation~~ feat(Algebra/Group/Even): Clean up file Jan 15, 2025

artie2000 mentioned this pull request Jan 15, 2025

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

Closed

3 tasks

improve some proofs

39ed89a

YaelDillies changed the title ~~feat(Algebra/Group/Even): Clean up file~~ chore(Algebra/Group/Even): Clean up file Jan 15, 2025

artie2000 added 2 commits January 18, 2025 03:06

Merge branch 'master' into artie2000-automate-even

5ece3c4

revert new lemmas

1bd56b3

YaelDillies reviewed Jan 22, 2025

View reviewed changes

Mathlib/Algebra/Field/Power.lean Outdated Show resolved Hide resolved

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

Mathlib/Algebra/Order/Field/Power.lean Outdated Show resolved Hide resolved

Mathlib/Data/Bool/Count.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 22, 2025

artie2000 and others added 6 commits January 22, 2025 23:39

Update Mathlib/Algebra/Field/Power.lean

b3c1d54

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Data/Bool/Count.lean

11aee9b

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Algebra/Group/Nat/Even.lean

854afc9

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update Mathlib/Algebra/Order/Field/Power.lean

4b1e14e

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

improve proof

9a23357

fix

3d62d3f

YaelDillies approved these changes Jan 23, 2025

View reviewed changes

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 23, 2025

adomani reviewed Jan 23, 2025

View reviewed changes

ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jan 23, 2025

artie2000 and others added 3 commits January 23, 2025 10:57

Update Mathlib/Algebra/Group/Even.lean

a75b2f9

Co-authored-by: damiano <adomani@gmail.com>

specify root

8c28c11

Merge branch 'artie2000-automate-even' of https://github.com/leanprov…

b5a3e9d

…er-community/mathlib4 into artie2000-automate-even

mathlib-bors bot changed the title ~~chore(Algebra/Group/Even): Clean up file~~ [Merged by Bors] - chore(Algebra/Group/Even): Clean up file Jan 23, 2025

mathlib-bors bot closed this Jan 23, 2025

mathlib-bors bot deleted the artie2000-automate-even branch January 23, 2025 12:19

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary b5a3e9dde1

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Uh oh!

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

Uh oh!

Uh oh!

YaelDillies commented Jan 16, 2025

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jan 23, 2025

Uh oh!

riccardobrasca commented Jan 23, 2025

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

adomani Jan 23, 2025

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 23, 2025

Uh oh!

adomani commented Jan 23, 2025

Uh oh!

artie2000 commented Jan 23, 2025

Uh oh!

YaelDillies commented Jan 23, 2025

Uh oh!

artie2000 commented Jan 23, 2025

Uh oh!

artie2000 commented Jan 23, 2025

Uh oh!

mathlib-bors bot commented Jan 23, 2025

Uh oh!

adomani commented Jan 23, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

artie2000 commented Jan 7, 2025 •

edited

Loading

github-actions bot commented Jan 7, 2025 •

edited

Loading

artie2000 commented Jan 13, 2025 •

edited

Loading

artie2000 commented Jan 16, 2025 •

edited

Loading