[Merged by Bors] - feat: instances for `ZeroHom` and `OneHom` by eric-wieser · Pull Request #27305 · leanprover-community/mathlib4

eric-wieser · 2025-07-20T13:40:23Z

This is motivated by wanting to write some lemmas about how the def in #27272 behaves on addition and scalar multiplcation, which requires these operations to first be defined.

This shows that ZeroHom forms an AddCommGroup and Module, as well as analogous intermediate statements and OneHom results.

depends on: [Merged by Bors] - chore(Algebra/Group/Hom/Instances): tidy and cancellativity #27318

github-actions · 2025-07-20T13:41:37Z

PR summary e71ae4c6d7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ OneHom.instCommGroup
+ OneHom.instCommMonoid
+ OneHom.instGroup
+ OneHom.instIntPow
+ OneHom.instMonoid
+ OneHom.instPow
+ OneHom.pow_apply
+ OneHom.zpow_apply
+ ZeroHom.instIntSMul
+ ZeroHom.instNatSMul
+ coe_div
+ coe_inv
+ coe_mul
+ coe_smul
+ div_apply
+ div_comp
+ instModule
+ instance [MonoidWithZero M] [MulActionWithZero M B] : MulActionWithZero M (ZeroHom A B)
+ instance [One M] [DivisionMonoid N] : Div (OneHom M N)
+ instance [One M] [InvOneClass N] : Inv (OneHom M N)
+ instance [One M] [MulOneClass N] : Mul (OneHom M N)
+ instance [One M] [MulOneClass N] [IsCancelMul N] : IsCancelMul (OneHom M N)
+ instance [One M] [MulOneClass N] [IsLeftCancelMul N] : IsLeftCancelMul (OneHom M N)
+ instance [One M] [MulOneClass N] [IsRightCancelMul N] : IsRightCancelMul (OneHom M N)
+ instance [SMul M N] [SMulZeroClass M B] [SMulZeroClass N B] [IsScalarTower M N B] :
+ instance [SMulZeroClass M B] : SMulZeroClass M (ZeroHom A B)
+ instance [SMulZeroClass M B] [SMulZeroClass Mᵐᵒᵖ B] [IsCentralScalar M B] :
+ instance [SMulZeroClass M B] [SMulZeroClass N B] [SMulCommClass M N B] :
+ instance [Zero M] [SMulWithZero M B] : SMulWithZero M (ZeroHom A B)
+ inv_apply
+ inv_comp
+ mul_apply
+ mul_comp
+ smul_apply
+ smul_comp

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 · 2025-07-23T09:39:24Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Algebra/Group/Hom/Instances): tidy and cancellativity #27318~~
By Dependent Issues (🤖). Happy coding!

…7386) This matches the Pi and Prod files in the same folder, and moves non-modules instances upstream to the `GroupWithZero` folder. The instances for AddMonoidHom have been generalized, the rest have been moved without changes. This is some cleanup ahead of #27305, which makes it clearer where the new `ZeroHom` instances there should go.

…-instances

Mathlib/Algebra/GroupWithZero/Action/Defs.lean

…anprover-community#27386) This matches the Pi and Prod files in the same folder, and moves non-modules instances upstream to the `GroupWithZero` folder. The instances for AddMonoidHom have been generalized, the rest have been moved without changes. This is some cleanup ahead of leanprover-community#27305, which makes it clearer where the new `ZeroHom` instances there should go.

YaelDillies

Thanks!

maintainer delegate

github-actions · 2025-08-14T14:22:38Z

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

Mathlib/Algebra/Group/Hom/Basic.lean

adomani

Thanks!

bors d+

mathlib-bors · 2025-08-14T14:56:10Z

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

…-instances

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

…-instances

ghost · 2025-09-06T09:49:37Z

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

This is motivated by wanting to write some lemmas about how the def in #27272 behaves on addition and scalar multiplcation, which requires these operations to first be defined. This shows that `ZeroHom` forms an `AddCommGroup` and `Module`, as well as analogous intermediate statements and `OneHom` results.

mathlib-bors · 2025-09-06T10:49:10Z

Pull request successfully merged into master.

Build succeeded:

CI Success

This is motivated by wanting to write some lemmas about how the def in leanprover-community#27272 behaves on addition and scalar multiplcation, which requires these operations to first be defined. This shows that `ZeroHom` forms an `AddCommGroup` and `Module`, as well as analogous intermediate statements and `OneHom` results.

eric-wieser added the WIP Work in progress label Jul 20, 2025

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

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 22, 2025

eric-wieser force-pushed the eric-wieser/zeroHom-instances branch from 83c9586 to 44c09ad Compare July 22, 2025 22:16

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jul 22, 2025

mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jul 23, 2025

eric-wieser added 3 commits July 23, 2025 09:40

feat: instances for ZeroHom

124ce39

action instances

b568b85

all the instances

651d639

eric-wieser force-pushed the eric-wieser/zeroHom-instances branch from 2fc0eed to 651d639 Compare July 23, 2025 09:40

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Jul 23, 2025

missing file

9b82962

eric-wieser mentioned this pull request Jul 23, 2025

[Merged by Bors] - chore(Algebra/GroupWithZero/Action/Hom): extract from other files #27386

Closed

remove assumptions

6afdc32

Merge remote-tracking branch 'origin/master' into eric-wieser/zeroHom…

d7280cd

…-instances

eric-wieser changed the title ~~feat: instances for ZeroHom~~ feat: instances for ZeroHom and OneHom Jul 23, 2025

eric-wieser removed the WIP Work in progress label Jul 23, 2025

eric-wieser commented Jul 23, 2025

View reviewed changes

Mathlib/Algebra/GroupWithZero/Action/Defs.lean Outdated Show resolved Hide resolved

grunweg assigned ericrbg Jul 31, 2025

YaelDillies approved these changes Aug 14, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 14, 2025

adomani reviewed Aug 14, 2025

View reviewed changes

Mathlib/Algebra/Group/Hom/Basic.lean Outdated Show resolved Hide resolved

adomani reviewed Aug 14, 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 Aug 14, 2025

eric-wieser and others added 3 commits August 14, 2025 15:28

Merge remote-tracking branch 'origin/master' into eric-wieser/zeroHom…

dba42ce

…-instances

Update Mathlib/Algebra/Group/Hom/Basic.lean

09c07a9

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

new syntax

0b513a9

eric-wieser added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label Sep 2, 2025

Merge remote-tracking branch 'origin/master' into eric-wieser/zeroHom…

e6057d4

…-instances

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

mathlib-bors bot changed the title ~~feat: instances for ZeroHom and OneHom~~ [Merged by Bors] - feat: instances for ZeroHom and OneHom Sep 6, 2025

mathlib-bors bot closed this Sep 6, 2025

mathlib-bors bot deleted the eric-wieser/zeroHom-instances branch September 6, 2025 10:49

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: instances for `ZeroHom` and `OneHom`#27305

[Merged by Bors] - feat: instances for `ZeroHom` and `OneHom`#27305
eric-wieser wants to merge 10 commits intomasterfrom
eric-wieser/zeroHom-instances

eric-wieser commented Jul 20, 2025 •

edited

Loading

Uh oh!

github-actions bot commented Jul 20, 2025 •

edited

Loading

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jul 23, 2025

Uh oh!

Uh oh!

YaelDillies left a comment

Uh oh!

github-actions bot commented Aug 14, 2025

Uh oh!

Uh oh!

adomani left a comment

Uh oh!

mathlib-bors bot commented Aug 14, 2025

Uh oh!

ghost commented Sep 6, 2025

Uh oh!

mathlib-bors bot commented Sep 6, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

eric-wieser commented Jul 20, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

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

Uh oh!

PR summary e71ae4c6d7

Import changes for modified files

Declarations diff

Uh oh!

mathlib4-dependent-issues-bot commented Jul 23, 2025

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Aug 14, 2025

Uh oh!

Uh oh!

adomani left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Aug 14, 2025

Uh oh!

ghost commented Sep 6, 2025

Uh oh!

mathlib-bors bot commented Sep 6, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

eric-wieser commented Jul 20, 2025 •

edited

Loading

github-actions bot commented Jul 20, 2025 •

edited

Loading