[Merged by Bors] - feat(Algebra/Group/Even): "Advanced" lemmas about even elements. by artie2000 · Pull Request #20272 · leanprover-community/mathlib4

artie2000 · 2024-12-27T11:26:39Z

Add construction of subgroup of even elements / squares.
Add result that squares (IsSquare) are non-negative.

These results cannot be added to Mathlib.Algebra.Group.Even directly because of import restrictions.
This PR is split off from #16094

depends on: [Merged by Bors] - chore(Algebra): rename theorems for consistency #20271 (uses new names)

github-actions · 2024-12-27T11:27:33Z

PR summary 3b54ab6da1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Group.Subgroup.Even` (new file)	346

Declarations diff

+ IsSquare.nonneg
+ squareIn_toSubmonoid
+ squareIn_toSubsemigroup
+++ coe_squareIn
+++ mem_squareIn
+++ squareIn

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

mathlib4-dependent-issues-bot · 2024-12-28T04:02:55Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Algebra): rename theorems for consistency #20271~~
By Dependent Issues (🤖). Happy coding!

YaelDillies · 2024-12-28T10:13:14Z

Advanced isn't really descriptive. What about Algebra.Group.Submonoid.Even?

artie2000 · 2024-12-28T15:47:44Z

Advanced isn't really descriptive. What about Algebra.Group.Submonoid.Even?

That sounds good, but I'm also adding the non-negativity result. Maybe that should go elsewhere? Not sure where the right home for it is. It can't go in Algebra.Group.Even due to import restrictions on order.

YaelDillies · 2024-12-28T17:52:41Z

What about a file under Algebra.Order.Group? Also note that the diff currently contains unrelated changes. Likely your last merge was botched somehow.

artie2000 · 2024-12-28T19:13:02Z

Uhh
I think I messed up the diff somehow
I was just trying to rebase onto the latest changes

artie2000 · 2024-12-28T19:50:47Z

What about a file under Algebra.Order.Group? Also note that the diff currently contains unrelated changes. Likely your last merge was botched somehow.

The lemma this is a variation on (mul_self_nonneg) is in Algebra.Order.Ring.Unbundled.Basic. However, import restrictions prevent me from putting the lemma directly into that file (Group.Even imports MonoidHom). Other files such as Algebra.Order.Ring.Basic are about bundled order typeclasses. I've put it at the top of Algebra.Order.Ring.Basic for now, but this doesn't feel like the right solution.

YaelDillies · 2024-12-28T21:46:13Z

I see you fiddle with Mathlib.lean quite a lot. Do you know about lake exe mk_all?

Mathlib/Algebra/Group/Subgroup/Even.lean

jcommelin

Thanks 🎉

bors merge

) Add construction of subgroup of even elements / squares. Add result that squares (`IsSquare`) are non-negative. These results cannot be added to `Mathlib.Algebra.Group.Even` directly because of import restrictions. This PR is split off from #16094

mathlib-bors · 2025-01-03T07:03:49Z

Build failed (retrying...):

Build

) Add construction of subgroup of even elements / squares. Add result that squares (`IsSquare`) are non-negative. These results cannot be added to `Mathlib.Algebra.Group.Even` directly because of import restrictions. This PR is split off from #16094

mathlib-bors · 2025-01-03T07:21:39Z

Build failed (retrying...):

Build

) Add construction of subgroup of even elements / squares. Add result that squares (`IsSquare`) are non-negative. These results cannot be added to `Mathlib.Algebra.Group.Even` directly because of import restrictions. This PR is split off from #16094

mathlib-bors · 2025-01-03T07:31:14Z

Pull request successfully merged into master.

Build succeeded:

Mathlib/Algebra/Group/Subgroup/Even.lean

* Follows on from #20272 * Rename some substructure constructions to align with `oneLE` / `nonneg` * Clarify some documentation Moves: * squareIn -> square * evenIn -> even * sumSqIn -> sumSq

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Dec 27, 2024

artie2000 requested review from YaelDillies and jcommelin December 27, 2024 11:27

artie2000 mentioned this pull request Dec 27, 2024

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

Closed

7 tasks

mathlib4-dependent-issues-bot added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Dec 27, 2024

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 Dec 28, 2024

artie2000 added 2 commits December 28, 2024 16:44

add + move

b092515

import fix

406491e

leanprover-community-bot-assistant 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 28, 2024

artie2000 force-pushed the artie2000-sq-advanced branch from 9d9d7f8 to 406491e Compare December 28, 2024 19:26

artie2000 added 3 commits December 28, 2024 19:55

move files around

0652869

docs

6b7aa61

fix?

d3acc8f

jcommelin reviewed Jan 2, 2025

View reviewed changes

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

artie2000 added 3 commits January 2, 2025 22:12

fix docs

4a114b0

register new to_additive naming rule

25eaac4

fix docs

3b54ab6

artie2000 added t-algebra Algebra (groups, rings, fields, etc) and removed awaiting-author A reviewer has asked the author a question or requested changes. new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! labels Jan 2, 2025

jcommelin reviewed Jan 3, 2025

View reviewed changes

ghost added the ready-to-merge This PR has been sent to bors. label Jan 3, 2025

mathlib-bors bot changed the title ~~feat(Algebra/Group/Even): "Advanced" lemmas about even elements.~~ [Merged by Bors] - feat(Algebra/Group/Even): "Advanced" lemmas about even elements. Jan 3, 2025

mathlib-bors bot closed this Jan 3, 2025

mathlib-bors bot deleted the artie2000-sq-advanced branch January 3, 2025 07:31

YaelDillies reviewed Jan 3, 2025

View reviewed changes

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

artie2000 mentioned this pull request Jan 3, 2025

[Merged by Bors] - chore(Algebra): make more names consistent #20449

Closed

Conversation

artie2000 commented Dec 27, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 27, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 3b54ab6da1

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Dec 28, 2024

Uh oh!

YaelDillies commented Dec 28, 2024

Uh oh!

artie2000 commented Dec 28, 2024

Uh oh!

YaelDillies commented Dec 28, 2024

Uh oh!

artie2000 commented Dec 28, 2024

Uh oh!

artie2000 commented Dec 28, 2024

Uh oh!

YaelDillies commented Dec 28, 2024

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 3, 2025

Uh oh!

mathlib-bors bot commented Jan 3, 2025

Uh oh!

mathlib-bors bot commented Jan 3, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

artie2000 commented Dec 27, 2024 •

edited

Loading

github-actions bot commented Dec 27, 2024 •

edited

Loading