[Merged by Bors] - refactor(Algebra/Algebra/Pi): cleanup and renaming by mistarro · Pull Request #21213 · leanprover-community/mathlib4

mistarro · 2025-01-29T09:45:26Z

Renaming and cleanup in Algebra.Algebra.Pi following discussion.

github-actions · 2025-01-29T09:46:23Z

PR summary 0852db481d

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ instance [∀ i, Algebra (S i) (A i)] : Algebra (Π i, S i) (Π i, A i)
- instance (g : I → Type*) [∀ i, CommSemiring (f i)] [∀ i, Semiring (g i)]

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

alreadydone

!bench

alreadydone · 2025-01-29T11:06:16Z

Mathlib/Algebra/Algebra/Pi.lean

+variable [CommSemiring R] [∀ i, Semiring (A i)] [∀ i, Algebra R (A i)]

-instance algebra {r : CommSemiring R} [s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)] :
-    Algebra R (∀ i : I, f i) where
-  algebraMap := (Pi.ringHom fun i => algebraMap R (f i) : R →+* ∀ i : I, f i)
+instance algebra : Algebra R (Π i, A i) where
+  algebraMap := (Pi.ringHom fun i => algebraMap R (A i) : R →+* Π i, A i)
  commutes' := fun a f => by ext; simp [Algebra.commutes]
  smul_def' := fun a f => by ext; simp [Algebra.smul_def]

-theorem algebraMap_def {_ : CommSemiring R} [_s : ∀ i, Semiring (f i)] [∀ i, Algebra R (f i)]
-    (a : R) : algebraMap R (∀ i, f i) a = fun i => algebraMap R (f i) a :=
+theorem algebraMap_def (a : R) : algebraMap R (Π i, A i) a = fun i => algebraMap R (A i) a :=


{_ : CommSemiring R} is different from [CommSemiring R] because (when you apply the theorem) the latter uses typeclass inference while the former uses unification. Please avoid changes that alter the semantics in a PR that's not supposed to do so.

Why should algebraMap_def use unification here? And all similar places? Just to speed up?
I think semantics is the same but the mechanism used to get arguments is different.

It changes the semantics in the sense that if a certain Algebra instance uses a non-canonical CommSemiring instance, then the current version of algebraMap_def will apply but yours will fail to apply. (IsScalarTower.of_algHom is an example of an IsScalarTower instance that uses a non-canonical Algebra instance).

I'm not sure about the reason to use unification for this particular lemma, but this was originally added by @kim-em in mathlib3#3463 and has been there for 4+ years.

Maybe something changed since then and we no longer need unification here? I mean, why binary (Cartesian) product would not use it but indexed product would? How did it look for the binary product back then?

Not sure why the previous !bench didn't go through. Since the original author hasn't responded with the intention, let's see the performance before deciding.

Sure, also we don't need to push this PR quickly through, we might wait for others to comment. Maybe someone would have an insight, I'm curious to learn here as well. Similar construction appears also for Algebra.Module.Pi.

alreadydone · 2025-01-29T14:01:17Z

!bench

leanprover-bot · 2025-01-29T14:29:46Z

Here are the benchmark results for commit 7cbd368.
There were no significant changes against commit abcae08.

github-actions · 2025-01-29T14:30:14Z

File	Instructions	%
`build`	-9.786⬝10⁹	(+0.00%)
CI run

alreadydone

The bench result looks good to me. Even though there are constructors of non-canonical CommSemiring instances, I'm not aware of them being used in global instances.
maintainer delegate

Mathlib/Algebra/Algebra/Pi.lean

github-actions · 2025-01-29T16:51:48Z

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

jcommelin

Thanks 🎉

bors d+

mathlib-bors · 2025-01-30T06:02:51Z

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

mistarro · 2025-01-31T09:06:05Z

bors r+

Renaming and cleanup in `Algebra.Algebra.Pi` following discussion.

mathlib-bors · 2025-01-31T09:33:05Z

Pull request successfully merged into master.

Build succeeded:

* factorial-dvd-int: (143 commits) Apply suggestions from code review feat(Factorial): k! divides the product of any k successive integers feat(CategoryTheory): creation of finite limits (#21320) chore: update Mathlib dependencies 2025-02-01 (#21328) chore(GroupTheory/SpecificGroups/Alternating.lean): follow last minute review of JX (#21314) feat: `‖x‖ₑ.toNNReal = ‖x‖₊` (#21306) chore: cleanup imports in Archive/IfNormalization (#21318) doc: fix several typos (#21315) feat(CategoryTheory): transfer being iso along an iso in the arrow category (#21310) chore: delete declarations deprecated between 2024-01 and 2024-07 (#21271) feat(Analysis/Normed/Module/Dual): polar in a normed space as a submodule (#20084) chore(Data/ZMod/Basic): split `ZMod.valMinAbs` off (#21308) feat(GroupTheory/Perm/Centralizer): study the centralizer of a permutation (#17522) feat(RingTheory/LocalRing): `IsLocalRing` for subrings (#21168) chore: update Mathlib dependencies 2025-02-01 (#21312) chore: update Mathlib dependencies 2025-01-31 (#21311) feat: generalize `mem_dite` to `Membership α β` (#21262) feat: Lemmas for some monomial orders (#16177) feat(CategoryTheory): the localized category is monoidal (#12728) feat: add function log⁺ (=positive part of the logarithm) and prove standard estimates (#21289) feat(RingTheory/WittVector): ring of Witt vectors is p-adically complete (#21295) feat(GroupTheory/GroupAction/Blocks): more on blocks (#21284) fix(FieldTheory/KrullTopology): make `krullTopology_discreteTopology_of_finiteDimensional` universe polymorphic (#21299) feat(RingTheory/Artinian): integral non-zero-divisors are units over artinian rings (#21199) refactor(Topology/Gluing): simplify definition of `TopCat.GlueData.Rel` (#20653) feat(RingTheory/PowerSeries): binomial series (#20192) chore(Mathlib/RingTheory/MvPolynomial): rename MonomiaOrder.lCoeff to MonomialOrder.leadingCoeff (#21290) chore (RingTheory/HahnSeries): fix names that use coeff (#21279) feat: let `notation3` distinguish `Prop` vs `Type _ ` vs `Sort _` (#21233) chore(MeasureTheory/Function/StronglyMeasurable): split Basic into Basic and AEStronglyMeasurable (#21273) feat(CategoryTheory): the monoidal category structure on a localization (#20951) feat(Analysis/Complex/Hadamard): generalize Hadamard's three lines theorem (#15009) feat(Order/CompleteBooleanAlgebra): Himp in terms of sSup (#20328) feat(ENNReal/Basic): add `ofNat_ne_top` and `top_ne_ofNat` (#14486) feat: Function.const as a PartialEquiv (#21137) chore(NonZeroDivisors): don't import rings (#20871) feat(Data/Set/Lattice): insert distributivity with iUnion/iInter (#21267) feat(GroupTheory/SpecificGroups/AlternatingGroup): subgroups of index 2 of Equiv.Perm (#21190) feat(GroupTheory/GroupAction/Transitive): basic results on transitive actions (#21285) perf(MeasureTheory/Function/LpSpace.lean): speed up (#21179) feat(Order): order isomorphisms from `Fin n` for small `n` (#21120) refactor(Topology/Group): turn morphisms in ProfiniteGrp into one field structures (#20740) feat: Sylow's first theorem for elementary `p`-groups (#21072) chore(Submonoid/Membership): don't import `MonoidWithZero` (#20748) refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213) feat(GroupTheory/IndexNormal): subgroups of small index are normal (#21186) feat(Algebra/Group/Action): add definition of equidecomposition (#16936) feat(CategoryTheory/Subpresheaf): equalizer (#21096) feat: add lemmas about products of `Matrix.stdBasisMatrix` (#21204) chore: update Mathlib dependencies 2025-01-31 (#21282) ...

Renaming and cleanup in `Algebra.Algebra.Pi` following discussion.

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

refactor(Algebra/Algebra/Pi): cleanup and renaming

7cbd368

mistarro force-pushed the mistarro/algebra-pi-cleanup branch from a2ac1f4 to 7cbd368 Compare January 29, 2025 09:52

alreadydone reviewed Jan 29, 2025

View reviewed changes

alreadydone approved these changes Jan 29, 2025

View reviewed changes

Mathlib/Algebra/Algebra/Pi.lean Outdated Show resolved Hide resolved

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

jcommelin reviewed Jan 30, 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 Jan 30, 2025

Use ↦ instead of =>.

0852db4

mathlib-bors bot pushed a commit that referenced this pull request Jan 31, 2025

refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213)

4e87722

Renaming and cleanup in `Algebra.Algebra.Pi` following discussion.

mathlib-bors bot changed the title ~~refactor(Algebra/Algebra/Pi): cleanup and renaming~~ [Merged by Bors] - refactor(Algebra/Algebra/Pi): cleanup and renaming Jan 31, 2025

mathlib-bors bot closed this Jan 31, 2025

mathlib-bors bot deleted the mistarro/algebra-pi-cleanup branch January 31, 2025 09:33

alreadydone mentioned this pull request Feb 2, 2025

[Merged by Bors] - refactor(FieldTheory): split Mathlib.FieldTheory.Purelyinseparable #21343

Closed

jt496 pushed a commit that referenced this pull request Feb 3, 2025

refactor(Algebra/Algebra/Pi): cleanup and renaming (#21213)

46a13c3

Renaming and cleanup in `Algebra.Algebra.Pi` following discussion.

Conversation

mistarro commented Jan 29, 2025

Uh oh!

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

Uh oh!

PR summary 0852db481d

Import changes for modified files

Declarations diff

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

alreadydone Jan 29, 2025

Choose a reason for hiding this comment

Uh oh!

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

Uh oh!

Choose a reason for hiding this comment

Uh oh!

alreadydone Jan 29, 2025

Choose a reason for hiding this comment

Uh oh!

mistarro Jan 29, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone Jan 29, 2025

Choose a reason for hiding this comment

Uh oh!

mistarro Jan 29, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone commented Jan 29, 2025

Uh oh!

leanprover-bot commented Jan 29, 2025

Uh oh!

github-actions bot commented Jan 29, 2025

Uh oh!

alreadydone left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Jan 29, 2025

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Jan 30, 2025

Uh oh!

mistarro commented Jan 31, 2025

Uh oh!

mathlib-bors bot commented Jan 31, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

github-actions bot commented Jan 29, 2025 •

edited

Loading

mistarro Jan 29, 2025 •

edited

Loading