Skip to content

chore: rename QuotientAddGroup.mk_out_eq_mul to mk_out_eq_add#41654

Open
adomani wants to merge 1 commit into
leanprover-community:masterfrom
adomani:to_additive-fix-mk_out_eq_add
Open

chore: rename QuotientAddGroup.mk_out_eq_mul to mk_out_eq_add#41654
adomani wants to merge 1 commit into
leanprover-community:masterfrom
adomani:to_additive-fix-mk_out_eq_add

Conversation

@adomani

@adomani adomani commented Jul 12, 2026

Copy link
Copy Markdown
Contributor

The additive lemma states (mk g).out = g + h, so by the to_additive naming convention its name should end in add, not mul. Renames it to QuotientAddGroup.mk_out_eq_add (a copy-paste error inherited from mathlib3) and deprecates the old name.

The additive lemma states `(mk g).out = g + h`, so by the `to_additive`
naming convention (`mul → add`) its name should end in `add`, not `mul`.
The `_mul` spelling is a long-standing copy-paste error inherited from
mathlib3 (the `#align quotient_add_group.mk_out'_eq_mul` from the original
port kept the multiplicative token when only the namespace was additivised).

Rename the additive declaration to `QuotientAddGroup.mk_out_eq_add` and keep
the old name as a deprecated alias.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@adomani adomani added the LLM-generated PRs with substantial input from LLMs - review accordingly label Jul 12, 2026
@github-actions

Copy link
Copy Markdown

PR summary 1ea2e3df23

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

+ QuotientAddGroup.mk_out_eq_mul

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.


No changes to strong technical debt.

No changes to weak technical debt.

Current commit 1ea2e3df23
Reference commit 2800ac2bd3

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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).

@github-actions github-actions Bot added the t-group-theory Group theory label Jul 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

LLM-generated PRs with substantial input from LLMs - review accordingly t-group-theory Group theory

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant