Skip to content

feat(GroupTheory/IndexNSmul): add results on multiplication-by-n in AddCommGroups#36494

Open
MichaelStollBayreuth wants to merge 18 commits intoleanprover-community:masterfrom
MichaelStollBayreuth:MS_API_index_2
Open

feat(GroupTheory/IndexNSmul): add results on multiplication-by-n in AddCommGroups#36494
MichaelStollBayreuth wants to merge 18 commits intoleanprover-community:masterfrom
MichaelStollBayreuth:MS_API_index_2

Conversation

@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

@MichaelStollBayreuth MichaelStollBayreuth commented Mar 11, 2026 •
edited
Loading

This PR adds a new file (to be able to have the required imports) that contains some results related to the (relative) index of subgroups in commutative additive groups and the multiplication-by-n map.

They will be useful in proving the Northcott property for heights on number fields.

Open in Gitpod

@MichaelStollBayreuth MichaelStollBayreuth added the t-algebra Algebra (groups, rings, fields, etc) label Mar 11, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 11, 2026 •
edited
Loading

PR summary 1a79483f50

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.GroupTheory.IndexNSmul (new file) 1413

Declarations diff

+ distribSMulToLinearMap_injective_of_isTorsionFree
+ finrank_eq_of_finiteIndex
+ finrank_eq_of_isFiniteRelIndex
+ index_nsmul
+ nsmulAddMonoidHom_injective_of_isTorsionFree
+ relIndex_nsmul

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/reporting/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-dependent-issues mathlib-dependent-issues bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 11, 2026
@mathlib-dependent-issues mathlib-dependent-issues bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 26, 2026
@mathlib-dependent-issues
Copy link
Copy Markdown

mathlib-dependent-issues bot commented Mar 26, 2026

This PR/issue depends on:

@artie2000
Copy link
Copy Markdown
Collaborator

artie2000 commented Apr 1, 2026

could you provide a more descriptive name for the PR?

@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor Author

MichaelStollBayreuth commented Apr 2, 2026

Is the PR description not good enough?

@artie2000
Copy link
Copy Markdown
Collaborator

artie2000 commented Apr 2, 2026

it's so people (like me) skimming the review queue can quickly decide whether we will understand the maths in your PR and decide to review it (or not)

@MichaelStollBayreuth MichaelStollBayreuth changed the title feat(GroupTheory/IndexNSmul): new file feat(GroupTheory/IndexNSmul): add results on multiplication-by-n in AddCommGroups Apr 2, 2026
dagurtomas
dagurtomas reviewed Apr 2, 2026
View reviewed changes
@dagurtomas dagurtomas added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 2, 2026
@MichaelStollBayreuth MichaelStollBayreuth removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 2, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@dagurtomas dagurtomas dagurtomas left review comments

Assignees

@dagurtomas dagurtomas

Labels

t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@MichaelStollBayreuth @artie2000 @dagurtomas