[Merged by Bors] - feat(to_dual): linter for redundant uses of `to_dual`/`to_additive` #33239

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Closed

JovanGerb wants to merge 13 commits into leanprover-community:master from JovanGerb:Jovan-to_dual-redundant

Collaborator

JovanGerb commented Dec 23, 2025

This PR adds a linter that helps avoid unneccessary uses of to_dual/to_additive. With to_dual self it can sometimes be hard to tell if it's actually doing anything or not, so this will help with that.


          feat(to_dual): linter for redundant uses of to_dual/to_additive

f93df3b

github-actions bot commented Dec 23, 2025 •

edited

Loading

PR summary bb55063693

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ Filter.Tendsto.enorm
+ Inseparable.enorm_eq_enorm
- not_lt_self

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

Collaborator

vihdzp commented Dec 23, 2025

As always I'd like to give thanks for the useful code, and express my regrets for being unable to review the metaprogramming.

bryangingechen self-assigned this

JovanGerb added 4 commits

December 23, 2025 20:54


          typo


          fixes

d5282ed


          update documentation on to_additive self

8e6791f


          extend linter message

mathlib4-merge-conflict-bot added the merge-conflict label

Collaborator

mathlib4-merge-conflict-bot commented Dec 29, 2025

This pull request has conflicts, please merge master and resolve them.


          Merge branch 'master' into Jovan-to_dual-redundant

2d5baa7

github-actions bot removed the merge-conflict label

mathlib4-merge-conflict-bot added the merge-conflict label

Collaborator

mathlib4-merge-conflict-bot commented Jan 1, 2026

This pull request has conflicts, please merge master and resolve them.


          Merge branch 'master' into Jovan-to_dual-redundant

55cdf56

github-actions bot removed the merge-conflict label


          fixes

51a0802

mathlib4-merge-conflict-bot added the merge-conflict label

Collaborator

mathlib4-merge-conflict-bot commented Jan 7, 2026

This pull request has conflicts, please merge master and resolve them.


          Merge branch 'master' into Jovan-to_dual-redundant

52c52ca

github-actions bot removed the merge-conflict label

mathlib4-merge-conflict-bot added the merge-conflict label

Collaborator

mathlib4-merge-conflict-bot commented Jan 9, 2026

This pull request has conflicts, please merge master and resolve them.


          Merge branch 'master' into Jovan-to_dual-redundant

7cfd3cf

github-actions bot removed the merge-conflict label

mathlib4-merge-conflict-bot added the merge-conflict label

Collaborator

mathlib4-merge-conflict-bot commented Jan 13, 2026

This pull request has conflicts, please merge master and resolve them.


          Merge branch 'master' into Jovan-to_dual-redundant

9fc97f0

github-actions bot removed the merge-conflict label

mathlib4-merge-conflict-bot added the merge-conflict label

Collaborator

mathlib4-merge-conflict-bot commented Jan 14, 2026

This pull request has conflicts, please merge master and resolve them.


          Merge branch 'master' into Jovan-to_dual-redundant

051c4c4

github-actions bot removed the merge-conflict label

JovanGerb commented

View reviewed changes

Mathlib/Analysis/Normed/Group/Continuity.lean

    
              @[to_additive Inseparable.enorm_eq_enorm]

              theorem Inseparable.enorm_eq_enorm' {E : Type*} [TopologicalSpace E] [ContinuousENorm E]

              theorem Inseparable.enorm_eq_enorm {E : Type*} [TopologicalSpace E] [ContinuousENorm E]

Collaborator Author

JovanGerb Jan 14, 2026

The primed version and unprimed version were literally the same thing. This was caught by the linter.

bryangingechen approved these changes

View reviewed changes

Contributor

bryangingechen left a comment

Thanks!
bors r+

leanprover-community-mathlib4-bot added the ready-to-merge label

mathlib-bors bot pushed a commit that referenced this pull request


          feat(to_dual): linter for redundant uses of to_dual/to_additive (#…

9f97bab

…33239)

This PR adds a linter that helps avoid unneccessary uses of `to_dual`/`to_additive`. With `to_dual self` it can sometimes be hard to tell if it's actually doing anything or not, so this will help with that.

Contributor

mathlib-bors bot commented Jan 14, 2026

Build failed:

Build

Contributor

bryangingechen commented Jan 14, 2026

bors d+

Contributor

mathlib-bors bot commented Jan 14, 2026

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

leanprover-community-mathlib4-bot added the delegated label

fix

Collaborator Author

JovanGerb commented Jan 14, 2026

bors r+

mathlib-bors bot pushed a commit that referenced this pull request


          feat(to_dual): linter for redundant uses of to_dual/to_additive (#…

a0ec5d2

…33239)

This PR adds a linter that helps avoid unneccessary uses of `to_dual`/`to_additive`. With `to_dual self` it can sometimes be hard to tell if it's actually doing anything or not, so this will help with that.

Contributor

mathlib-bors bot commented Jan 14, 2026

Pull request successfully merged into master.

Build succeeded:

mathlib-bors bot changed the title ~~feat(to_dual): linter for redundant uses of to_dual/to_additive~~ [Merged by Bors] - feat(to_dual): linter for redundant uses of to_dual/to_additive

mathlib-bors bot closed this

adomani mentioned this pull request

feat: MiM PR report #15355

Open

eliasjudin pushed a commit to eliasjudin/mathlib4 that referenced this pull request


          feat(to_dual): linter for redundant uses of to_dual/to_additive (l…

a4558cd

…eanprover-community#33239)

This PR adds a linter that helps avoid unneccessary uses of `to_dual`/`to_additive`. With `to_dual self` it can sometimes be hard to tell if it's actually doing anything or not, so this will help with that.

goliath-klein pushed a commit to PrParadoxy/mathlib4 that referenced this pull request


          feat(to_dual): linter for redundant uses of to_dual/to_additive (l…

fd17a10

…eanprover-community#33239)

This PR adds a linter that helps avoid unneccessary uses of `to_dual`/`to_additive`. With `to_dual self` it can sometimes be hard to tell if it's actually doing anything or not, so this will help with that.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

delegated ready-to-merge