feat(Algebra/Group/Even): "Advanced" lemmas about even elements.

[artie2000]

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]

PR summary d3acc8fce2

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

---

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]

This PR/issue depends on:

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

[YaelDillies]

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

[artie2000]

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]

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]

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

[artie2000]

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]

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