[Merged by Bors] - feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodule versions of ltAddSubgroup#26829

Closed

pechersky wants to merge 20 commits intoleanprover-community:masterfrom

pechersky:valuation-ltideal-defns

Contributor

pechersky commented Jul 6, 2025

Extracted from #25450 without changing how Valued works

@faenuccio hopefully this bypasses any wait on #14752 because I am not changing Valued files.

pechersky added 13 commits

June 4, 2025 10:56


          feat(Valued): Valuation.leAddSubgroup and ideal/submodule versions of…

0777b04

… ltAddSubgroup

Also golf existing proofs


          golf with mono

01e9b07


          another order lemma

f48c530


          submodule and ideals

436180c


          deprecate spelling


          clopen

7fd0761


          zero

a5b05a9


          fix comment


          v_le_of_mem

72ce4c5


          golf

5974c67


          move ideal and submodule defns to Valuation namespace

ae61e80

doesn't require Valued


          Merge remote-tracking branch 'upstream/master' into valuation-ltideal

a16dee6


          reset back

c6632ca

This was referenced Jul 6, 2025

feat(Valued): Valuation.leAddSubgroup and ideal/submodule versions of ltAddSubgroup #25450

Closed

feat(Topology/Algebra/Valued): IsLinearTopology 𝒪[K] K and 𝒪[K] 𝒪[K] #24627

Open

github-actions bot commented Jul 6, 2025 •

edited

Loading

PR summary 9fd7af820a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ leAddSubgroup
+ leAddSubgroup_monotone
+ leAddSubgroup_zero
+ leIdeal
+ leIdeal_map_algebraMap_eq_leSubmodule_min
+ leIdeal_mono
+ leIdeal_v_le_of_mem
+ leIdeal_zero
+ leSubmodule
+ leSubmodule_comap_algebraMap_eq_leIdeal
+ leSubmodule_monotone
+ leSubmodule_v_le_of_mem
+ leSubmodule_zero
+ ltAddSubgroup_le_leAddSubgroup
+ ltAddSubgroup_monotone
+ ltIdeal
+ ltIdeal_le_leIdeal
+ ltIdeal_mono
+ ltIdeal_v_le_of_mem
+ ltSubmodule
+ ltSubmodule_le_leSubmodule
+ ltSubmodule_monotone
+ ltSubmodule_v_le_of_mem
+ mem_leAddSubgroup_iff
+ mem_leIdeal_iff
+ mem_leSubmodule_iff
+ mem_ltIdeal_iff
+ mem_ltSubmodule_iff

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

github-actions bot added the t-algebra label


          lint

121deef

pechersky mentioned this pull request

feat(RingTheory/Valuation): define ball, closed ball, and sphere #27451

Open

JovanGerb reviewed

View reviewed changes

Mathlib/RingTheory/Valuation/Integers.lean Outdated Show resolved Hide resolved


          rename

0a1e3d9

grunweg added t-ring-theory and removed t-algebra labels

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

Collaborator

mathlib4-merge-conflict-bot commented Aug 8, 2025

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


          Merge remote-tracking branch 'upstream/master' into valuation-ltideal…

f1b6ace

…-defns

github-actions bot removed the merge-conflict label


          fix naming

cbe1ebb

leanprover-community-bot-assistant assigned mariainesdff

mariainesdff reviewed

View reviewed changes

Mathlib/RingTheory/Valuation/Integers.lean Outdated Show resolved Hide resolved

mariainesdff reviewed

View reviewed changes

Mathlib/RingTheory/Valuation/Integers.lean Outdated Show resolved Hide resolved

mariainesdff reviewed

View reviewed changes

Mathlib/RingTheory/Valuation/Integers.lean Outdated Show resolved Hide resolved

pechersky and others added 3 commits

September 19, 2025 12:02


          Apply suggestions from code review

b551d7f

Co-authored-by: María Inés de Frutos-Fernández <88536493+mariainesdff@users.noreply.github.com>


          golf

6be1bc6


          Merge branch 'master' into valuation-ltideal-defns

a8e141d

Contributor

mariainesdff commented Oct 22, 2025

Thanks!
maintainer merge

github-actions bot commented Oct 22, 2025

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

ghost added the maintainer-merge label

Member

riccardobrasca commented Oct 22, 2025

Thanks!

bors merge

ghost added ready-to-merge and removed maintainer-merge labels

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


          feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodu…

59577da

…le versions of ltAddSubgroup (#26829)

Extracted from #25450 without changing how Valued works

Contributor

mathlib-bors bot commented Oct 22, 2025

Build failed (retrying...):

Post-Build Step

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


          feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodu…

6692d93

…le versions of ltAddSubgroup (#26829)

Extracted from #25450 without changing how Valued works

Contributor

mathlib-bors bot commented Oct 22, 2025

Build failed (retrying...):

Lint style

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


          feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodu…

7b3713f

…le versions of ltAddSubgroup (#26829)

Extracted from #25450 without changing how Valued works

Contributor

mathlib-bors bot commented Oct 22, 2025

Build failed (retrying...):

Post-Build Step

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


          feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodu…

0b35383

…le versions of ltAddSubgroup (#26829)

Extracted from #25450 without changing how Valued works

Contributor

mathlib-bors bot commented Oct 22, 2025

This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried.

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


          feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodu…

b41214d

…le versions of ltAddSubgroup (#26829)

Extracted from #25450 without changing how Valued works

Contributor

mathlib-bors bot commented Oct 22, 2025

Build failed (retrying...):

Post-Build Step

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


          feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodu…

599f81d

…le versions of ltAddSubgroup (#26829)

Extracted from #25450 without changing how Valued works

Contributor

mathlib-bors bot commented Oct 23, 2025

Pull request successfully merged into master.

Build succeeded:

mathlib-bors bot changed the title ~~feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodule versions of ltAddSubgroup~~ [Merged by Bors] - feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodule versions of ltAddSubgroup

mathlib-bors bot closed this

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


          feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodu…

2d436a2

…le versions of ltAddSubgroup (leanprover-community#26829)

Extracted from leanprover-community#25450 without changing how Valued works

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


          feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodu…

242121f

…le versions of ltAddSubgroup (leanprover-community#26829)

Extracted from leanprover-community#25450 without changing how Valued works

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


          feat(RingTheory/Valuation): Valuation.leAddSubgroup and ideal/submodu…

b592a85

…le versions of ltAddSubgroup (leanprover-community#26829)

Extracted from leanprover-community#25450 without changing how Valued works

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

Labels

ready-to-merge t-ring-theory