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

artie2000 · 2025-01-03T17:08:30Z

Follows on from [Merged by Bors] - feat(Algebra/Group/Even): "Advanced" lemmas about even elements. #20272
Rename some substructure constructions to align with oneLE / nonneg
Clarify some documentation

Moves:

squareIn -> square
evenIn -> even
sumSqIn -> sumSq

github-actions · 2025-01-03T17:09:48Z

PR summary 02c70f3aea

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ mem_sumSq_of_isSquare
+ square_toSubmonoid
+ square_toSubsemigroup
+ sumSq
+++ coe_square
+++ mem_square
+++ square
- 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).

Mathlib/Algebra/Group/Subgroup/Even.lean

Mathlib/Algebra/Order/Group/Cone.lean

artie2000 · 2025-01-03T18:11:40Z

Part reverted, split to #20451, diffs should be cleaner now.

YaelDillies

Thanks!

maintainer delegate

YaelDillies · 2025-01-03T18:16:13Z

Mathlib/Algebra/Group/Subgroup/Even.lean

@@ -13,73 +13,73 @@ This file defines the subgroup of squares / even elements in an abelian group.
 -/

 namespace Subsemigroup
-variable {S : Type*} [CommSemigroup S] {a : S}
+variable {S : Type*} [CommSemigroup S]


This feels like a regression

I thought it would be silly to have that there for the sake of 1 lemma

github-actions · 2025-01-03T18:17:09Z

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

Ruben-VandeVelde · 2025-01-03T21:39:15Z

Mathlib/Algebra/Group/Subgroup/Even.lean

-def squareIn : Subsemigroup S where
+"In a commutative additive semigroup `S`, `AddSubsemigroup.even S`
+is the subsemigroup of even elements in `S`."]
+def square : Subsemigroup S where


I don't see the deprecations for these changes?

They were just added yesterday or today

Yeah, this PR follows a comment @YaelDillies made about the naming in #20272, after that PR was already on the maintainer queue

jcommelin · 2025-01-06T09:57:25Z

I'm confused that the latest commit has a ❎ even though the overall CI seems to be ✔️ .

jcommelin

bors d+

mathlib-bors · 2025-01-06T09:57:47Z

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

YaelDillies · 2025-01-06T10:12:21Z

I'm confused that the latest commit has a ❎ even though the overall CI seems to be ✔️ .

It's written "artie2000 added a commit that referenced this pull request", not "artie2000 added a commit". The commit in question does not belong to this branch

artie2000 · 2025-01-06T17:01:34Z

bors r+

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

mathlib-bors · 2025-01-06T17:10:43Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (189 commits) chore(Algebra): make more names consistent (#20449) feat: Polynomial FLT (#18882) feat: A disjoint union is finite iff all sets are finite, and all but finitely many are empty (#20457) fix: linkfix in 100.yaml (#20517) feat(1000): fill in more entries (#20470) feat(Combinatorics/SimpleGraph/Walk): add `penultimate` and `snd` (#16769) feat(ContinuousMultilinearMap): add lemmas about `.prod` (#20462) feat(RingTheory): classification of etale algebras over fields (#20324) fix: Allow multiple builds on staging branch (#20515) feat(CategoryTheory/Shift/Adjunction): properties of `Adjunction.CommShift` (#20337) chore(Data/Multiset/Basic): move the `sub`, `union`, `inter` sections lower (#19863) chore(Topology/UniformSpace/Completion): make coe' argument implicit (#20514) refactor(Algebra/Category/Grp/Colimits): change the construction of colimits in `AddCommGrp` (#20474) feat(Topology/Algebra/InfiniteSum/NatInt): Add pnat lems (#16544) chore(RingTheory/Finiteness): rename Module.Finite.out (#20506) refactor(CategoryTheory/Limits/Preserves/Ulift): simplify the proof that the universe lifting functor for types preserves all colimits (#20508) feat(CategoryTheory): products in the category of Ind-objects (#20507) chore: remove >9 month old deprecations (#20505) chore(FieldTheory/Galois): small cleanup (#20217) chore(LinearIndependent): generalize to semirings (#20480) chore(NumberTheory/NumberField/AdeleRing): refactor adele rings (#20500) chore: replace `aesop` with `simp` where possible (#20483) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) ...

artie2000 added 2 commits January 3, 2025 17:02

rename, fix, make consistent

4880113

deprecate

b1330d6

artie2000 requested a review from YaelDillies January 3, 2025 17:08

artie2000 mentioned this pull request Jan 3, 2025

[Merged by Bors] - feat(Algebra/Group/Even): "Advanced" lemmas about even elements. #20272

Closed

1 task

artie2000 mentioned this pull request Jan 3, 2025

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

Closed

7 tasks

fix

4e6057c

YaelDillies reviewed Jan 3, 2025

View reviewed changes

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

Mathlib/Algebra/Order/Group/Cone.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Order/Group/Cone.lean Outdated Show resolved Hide resolved

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

artie2000 added 3 commits January 3, 2025 17:41

fix docs

5b40b38

part revert

21eb62d

part revert cont

02c70f3

artie2000 removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 3, 2025

YaelDillies approved these changes Jan 3, 2025

View reviewed changes

github-actions bot added the maintainer-merge label Jan 3, 2025

Ruben-VandeVelde reviewed Jan 3, 2025

View reviewed changes

artie2000 added a commit that referenced this pull request Jan 4, 2025

#20449 rename

d2259b5

artie2000 requested review from Ruben-VandeVelde and jcommelin January 4, 2025 17:29

jcommelin reviewed Jan 6, 2025

View reviewed changes

leanprover-community-mathlib4-bot added the delegated label Jan 6, 2025

mathlib-bors bot changed the title ~~chore(Algebra): make more names consistent~~ [Merged by Bors] - chore(Algebra): make more names consistent Jan 6, 2025

mathlib-bors bot closed this Jan 6, 2025

mathlib-bors bot deleted the artie2000-remove-in branch January 6, 2025 17:10

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

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

artie2000 commented Jan 3, 2025 •

edited

Loading

github-actions bot commented Jan 3, 2025 •

edited

Loading

Declarations diff

artie2000 commented Jan 3, 2025

YaelDillies left a comment

YaelDillies Jan 3, 2025

artie2000 Jan 3, 2025

github-actions bot commented Jan 3, 2025

Ruben-VandeVelde Jan 3, 2025

YaelDillies Jan 3, 2025

artie2000 Jan 3, 2025

jcommelin commented Jan 6, 2025

jcommelin left a comment

mathlib-bors bot commented Jan 6, 2025

YaelDillies commented Jan 6, 2025

artie2000 commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

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

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

Conversation

artie2000 commented Jan 3, 2025 • edited Loading

github-actions bot commented Jan 3, 2025 • edited Loading

PR summary 02c70f3aea

Import changes for modified files

Declarations diff

artie2000 commented Jan 3, 2025

YaelDillies left a comment

Choose a reason for hiding this comment

YaelDillies Jan 3, 2025

Choose a reason for hiding this comment

artie2000 Jan 3, 2025

Choose a reason for hiding this comment

github-actions bot commented Jan 3, 2025

Ruben-VandeVelde Jan 3, 2025

Choose a reason for hiding this comment

YaelDillies Jan 3, 2025

Choose a reason for hiding this comment

artie2000 Jan 3, 2025

Choose a reason for hiding this comment

jcommelin commented Jan 6, 2025

jcommelin left a comment

Choose a reason for hiding this comment

mathlib-bors bot commented Jan 6, 2025

YaelDillies commented Jan 6, 2025

artie2000 commented Jan 6, 2025

mathlib-bors bot commented Jan 6, 2025

artie2000 commented Jan 3, 2025 •

edited

Loading

github-actions bot commented Jan 3, 2025 •

edited

Loading