[Merged by Bors] - feat(Algebra): saturation of a submonoid by kckennylau · Pull Request #31132 · leanprover-community/mathlib4

kckennylau · 2025-10-31T21:53:45Z

This PR defines the saturation of a submonoid and the type of saturated submonoids.

It is used for the context of localisations.

Caveat: there is a similarly named predicate called AddSubgroup.Saturated.

Zulip:

github-actions · 2025-10-31T21:54:52Z

PR summary 0fbcb39f55

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Algebra.Group.Submonoid.Saturation` (new file)	418

Declarations diff

+ AddSubgroup.Saturated
+ AddSubgroup.ker_saturated
+ AddSubgroup.saturated_iff_nsmul
+ MulSaturated
+ PowSaturated
+ SaturatedAddSubmonoid
+ SaturatedSubmonoid
+ Subgroup.Saturated
+ Subgroup.saturated_iff_npow
+ bot_def
+ ext
+ ext'
+ gc_saturation
+ giSaturation
+ iInf
+ iSup_def
+ inf
+ instance (M : Type*) [MulOneClass M] :
+ instance : CompleteSemilatticeInf (SaturatedSubmonoid M)
+ instance : InfSet (SaturatedSubmonoid M)
+ instance : Min (SaturatedSubmonoid M)
+ instance : PartialOrder (SaturatedSubmonoid M) := .ofSetLike ..
+ instance : SetLike (SaturatedSubmonoid M) M
+ instance : SubmonoidClass (SaturatedSubmonoid M) M
+ instance : Top (SaturatedSubmonoid M)
+ le_toSubmonoid_saturation
+ mem_bot_iff
+ mem_sInf
+ mem_saturation_iff
+ mem_saturation_iff'
+ mem_saturation_iff_exists_dvd
+ mem_toSubmonoid
+ mem_top
+ mul_mem_iff
+ of_left
+ of_right
+ powSaturated_iff_npow
+ sInf
+ sSup_def
+ saturation
+ saturation_bot
+ saturation_iSup
+ saturation_induction
+ saturation_le_iff_le
+ saturation_le_of_le
+ saturation_sSup
+ saturation_sup
+ saturation_toSubmonoid
+ saturation_top
+ sup_def
+ toSubmonoid_injective
+ top
- Saturated
- saturated_iff_npow

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/Algebra/Group/Submonoid/Saturation.lean

mathlib4-merge-conflict-bot · 2025-11-19T08:19:41Z

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

b-mehta

We also have Subgroup.Saturated, which is a mathematically different notion, and the file defining it is not imported anywhere. It looks like the literature prefers this notion for the name "saturated". @jcommelin could you say something about what Subgroup.Saturated was useful for (as the author of the file)?

kckennylau · 2026-03-02T11:48:45Z

@b-mehta @jcommelin leanprover-community/mathlib3#8137 it was for liquid tensor

kckennylau · 2026-03-02T11:55:16Z

https://github.com/leanprover-community/lean-liquid/blob/087fffad55dc1dd8d54ab35c9816926a45b8c0fd/src/polyhedral_lattice/quotient.lean#L32

riccardobrasca

Is there a reason why you are not additivizing everything?

Mathlib/Algebra/Group/Submonoid/Saturation.lean

kckennylau · 2026-03-03T10:48:17Z

I'll additivize it.

Mathlib/GroupTheory/Subgroup/Saturated.lean

Mathlib/Algebra/Group/Submonoid/Saturation.lean

kbuzzard · 2026-03-03T16:10:46Z

bors d+

mathlib-bors · 2026-03-03T16:10:49Z

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

Co-authored-by: Kevin Buzzard <[email protected]>

kckennylau · 2026-03-03T16:13:13Z

bors r+

bryangingechen · 2026-03-03T16:32:30Z

bors r+

This PR defines the saturation of a submonoid and the type of saturated submonoids. It is used for the context of localisations. Caveat: there is a similarly named predicate called `AddSubgroup.Saturated`. Zulip: * [mathlib4 > saturation of a submonoid](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/saturation.20of.20a.20submonoid/with/548242862) * [#Is there code for X? > Closure of Submonoid in CommMonoids](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Closure.20of.20Submonoid.20in.20CommMonoids/near/419087778)

mathlib-bors · 2026-03-03T16:46:54Z

Pull request successfully merged into master.

Build succeeded:

This PR defines the saturation of a submonoid and the type of saturated submonoids. It is used for the context of localisations. Caveat: there is a similarly named predicate called `AddSubgroup.Saturated`. Zulip: * [mathlib4 > saturation of a submonoid](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/saturation.20of.20a.20submonoid/with/548242862) * [#Is there code for X? > Closure of Submonoid in CommMonoids](https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Closure.20of.20Submonoid.20in.20CommMonoids/near/419087778)

Feat(Algebra): saturation of a submonoid

fcda558

kckennylau requested review from alreadydone, plp127 and urkud October 31, 2025 21:54

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

endow

f54aaca

kckennylau mentioned this pull request Oct 31, 2025

feat(RingTheory): is localization iff is localization on saturation #31135

Open

1 task

sync with leanprover-community#31135

bfa4d74

plp127 reviewed Oct 31, 2025

View reviewed changes

Mathlib/Algebra/Group/Submonoid/Saturation.lean Outdated Show resolved Hide resolved

plp127 reviewed Nov 1, 2025

View reviewed changes

Mathlib/Algebra/Group/Submonoid/Saturation.lean Outdated Show resolved Hide resolved

generalise

d74ef76

plp127 reviewed Nov 1, 2025

View reviewed changes

Mathlib/Algebra/Group/Submonoid/Saturation.lean Outdated Show resolved Hide resolved

leanprover-community-bot-assistant assigned kim-em Nov 8, 2025

mathlib4-merge-conflict-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 19, 2025

Merge branch 'master' into monoid-saturation

0d4b976

github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 20, 2025

alreadydone changed the title ~~Feat(Algebra): saturation of a submonoid~~ feat(Algebra): saturation of a submonoid Nov 28, 2025

Merge remote-tracking branch 'origin/master' into monoid-saturation

817fe44

b-mehta reviewed Mar 2, 2026

View reviewed changes

kckennylau added 2 commits March 3, 2026 10:20

rename existing saturated to Pow/NSMulSaturated

4bdf05a

docstring, remove induction default

be34f04

riccardobrasca reviewed Mar 3, 2026

View reviewed changes

Mathlib/Algebra/Group/Submonoid/Saturation.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/Group/Submonoid/Saturation.lean Outdated Show resolved Hide resolved

docstring

04a2c8f

additivize

bf8075a

kbuzzard reviewed Mar 3, 2026

View reviewed changes

Mathlib/GroupTheory/Subgroup/Saturated.lean Outdated Show resolved Hide resolved

kbuzzard reviewed Mar 3, 2026

View reviewed changes

Mathlib/Algebra/Group/Submonoid/Saturation.lean Outdated Show resolved Hide resolved

kbuzzard reviewed Mar 3, 2026

View reviewed changes

Mathlib/Algebra/Group/Submonoid/Saturation.lean Outdated Show resolved Hide resolved

kbuzzard reviewed Mar 3, 2026

View reviewed changes

Mathlib/Algebra/Group/Submonoid/Saturation.lean Outdated Show resolved Hide resolved

kbuzzard reviewed Mar 3, 2026

View reviewed changes

Mathlib/Algebra/Group/Submonoid/Saturation.lean Show resolved Hide resolved

style fixes

a1a06e1

mathlib-triage bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 3, 2026

Apply suggestions from code review

7cb57de

Co-authored-by: Kevin Buzzard <[email protected]>

mathlib-triage bot added the ready-to-merge This PR has been sent to bors. label Mar 3, 2026

mathlib-bors bot changed the title ~~feat(Algebra): saturation of a submonoid~~ [Merged by Bors] - feat(Algebra): saturation of a submonoid Mar 3, 2026

mathlib-bors bot closed this Mar 3, 2026

Conversation

kckennylau commented Oct 31, 2025

Uh oh!

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

Uh oh!

PR summary 0fbcb39f55

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Nov 19, 2025

Uh oh!

b-mehta left a comment

Choose a reason for hiding this comment

Uh oh!

kckennylau commented Mar 2, 2026

Uh oh!

kckennylau commented Mar 2, 2026

Uh oh!

riccardobrasca left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

kckennylau commented Mar 3, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kbuzzard commented Mar 3, 2026

Uh oh!

mathlib-bors bot commented Mar 3, 2026

Uh oh!

kckennylau commented Mar 3, 2026

Uh oh!

bryangingechen commented Mar 3, 2026

Uh oh!

mathlib-bors bot commented Mar 3, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

github-actions bot commented Oct 31, 2025 •

edited

Loading