[Merged by Bors] - feat(RingTheory/Ideal): generalize Submodule.colon to sets #33390

farmanb · 2025-12-29T21:42:59Z

This PR generalizes Submodule.colon to arguments of type Set M in the second slot and updates the surrounding API accordingly.

Main changes

Generalize Submodule.colon to take S : Set M rather than P : Submodule R M.
Normalize theorems/lemmas to use Set.univ instead of ⊤ where appropriate.
Strengthen iInf_colon_iSup by removing an unnecessary commutativity assumption.
Update monotonicity and inclusion lemmas (e.g. _root_.Ideal.le_colon) to use set inclusions.
Add colon_bot' (CommSemiring): identify ⊥.colon S with the annihilator of Submodule.span R S.
Adjust annihilator-related proofs to account for the generalized colon, using explicit coercions such as Submodule.top_coe.

…alization * Update IsTwoSided instance to apply only to submodules via coercion to sets. * Normalize statements to use Set.univ (avoiding ⊤) and fix monotonicity arguments accordingly. * Remove colon_inf_left in favor of direct use of iInf_colon_iSup. * Rework colon_inf_eq_left_of_le to use the generalized API. * Add colon_bot' (CommSemiring): identify ⊥.colon S with the annihilator of span S. * Tidy annihilator lemmas (Submodule.top_coe) and related rewrites.

github-actions · 2025-12-29T21:44:15Z

PR summary 19e41d0839

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ _root_.Ideal.colon_span
+ _root_.Ideal.mem_colon_span_singleton
+ bot_colon
+ bot_colon'
+ colon_empty
+ colon_eq_top_iff_subset
+ colon_iUnion
+ colon_inf_eq_left_of_subset
+ colon_span
+ colon_union
+ colon_univ
+ iInf_colon
+ iInf_colon_iUnion
+ inf_colon
+ instance (priority := low) (P : Submodule R M) : (N.colon (P : Set M)).IsTwoSided
+ mem_colon_span_singleton
+ top_colon
- _root_.Ideal.mem_colon_singleton
- instance (priority := low) : (N.colon P).IsTwoSided

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

farmanb · 2026-01-08T20:05:18Z

-WIP

Mathlib/RingTheory/Ideal/Colon.lean

erdOne · 2026-01-10T16:10:34Z

Sorry didn't notice this because it was tagged WIP 😅

…_colon

…n_iUnion

…_eq_top_of_subset

…pt proof to iUnion

…on_span_singleton

farmanb · 2026-01-11T19:55:47Z

-awaiting-author

Mathlib/RingTheory/Ideal/Colon.lean

…with alias

…emmas

…em_colon_singleton

…unused declarations

Mathlib/RingTheory/Ideal/Colon.lean

Mathlib/RingTheory/Lasker.lean

Mathlib/RingTheory/Ideal/Colon.lean

erdOne

LGTM otherwise

Thanks!
maintainer merge

github-actions · 2026-01-15T23:43:45Z

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

…sPrimary

riccardobrasca · 2026-01-16T06:00:18Z

Thanks!

bors d+

mathlib-bors · 2026-01-16T06:00:21Z

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

farmanb · 2026-01-16T10:21:32Z

Thanks!

bors r+

This PR generalizes `Submodule.colon` to arguments of type `Set M` in the second slot and updates the surrounding API accordingly. Main changes * Generalize `Submodule.colon` to take `S : Set M` rather than `P : Submodule R M`. * Normalize theorems/lemmas to use `Set.univ` instead of `⊤` where appropriate. * Strengthen `iInf_colon_iSup` by removing an unnecessary commutativity assumption. * Update monotonicity and inclusion lemmas (e.g. `_root_.Ideal.le_colon`) to use set inclusions. * Add `colon_bot'` (`CommSemiring`): identify `⊥.colon S` with the annihilator of `Submodule.span R S`. * Adjust annihilator-related proofs to account for the generalized colon, using explicit coercions such as `Submodule.top_coe`. Co-authored-by: blake-farman <blake.farman@gmail.com>

mathlib-bors · 2026-01-16T12:20:41Z

Build failed (retrying...):

Post-Build Step

This PR generalizes `Submodule.colon` to arguments of type `Set M` in the second slot and updates the surrounding API accordingly. Main changes * Generalize `Submodule.colon` to take `S : Set M` rather than `P : Submodule R M`. * Normalize theorems/lemmas to use `Set.univ` instead of `⊤` where appropriate. * Strengthen `iInf_colon_iSup` by removing an unnecessary commutativity assumption. * Update monotonicity and inclusion lemmas (e.g. `_root_.Ideal.le_colon`) to use set inclusions. * Add `colon_bot'` (`CommSemiring`): identify `⊥.colon S` with the annihilator of `Submodule.span R S`. * Adjust annihilator-related proofs to account for the generalized colon, using explicit coercions such as `Submodule.top_coe`. Co-authored-by: blake-farman <blake.farman@gmail.com>

mathlib-bors · 2026-01-16T15:16:43Z

Pull request successfully merged into master.

Build succeeded:

This adapts IdealFilter to the generalized Submodule.colon API introduced in leanprover-community#33390.

…r-community#33390) This PR generalizes `Submodule.colon` to arguments of type `Set M` in the second slot and updates the surrounding API accordingly. Main changes * Generalize `Submodule.colon` to take `S : Set M` rather than `P : Submodule R M`. * Normalize theorems/lemmas to use `Set.univ` instead of `⊤` where appropriate. * Strengthen `iInf_colon_iSup` by removing an unnecessary commutativity assumption. * Update monotonicity and inclusion lemmas (e.g. `_root_.Ideal.le_colon`) to use set inclusions. * Add `colon_bot'` (`CommSemiring`): identify `⊥.colon S` with the annihilator of `Submodule.span R S`. * Adjust annihilator-related proofs to account for the generalized colon, using explicit coercions such as `Submodule.top_coe`. Co-authored-by: blake-farman <blake.farman@gmail.com>

blake-farman added 3 commits December 29, 2025 12:04

feat(RingTheory/Ideal/Colon): generalize Submodule.colon to Set

c468b59

refactor(RingTheory): adapt to Submodule.colon Set generalization

bd0a7e5

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-ring-theory Ring theory labels Dec 29, 2025

github-actions bot added the WIP Work in progress label Dec 29, 2025

farmanb mentioned this pull request Dec 29, 2025

[Merged by Bors] - feat(RingTheory/IdealFilter): add ideal filters and Gabriel filters #33021

Closed

1 task

farmanb marked this pull request as ready for review December 30, 2025 15:30

github-actions bot removed the WIP Work in progress label Jan 8, 2026

erdOne reviewed Jan 10, 2026

View reviewed changes

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 10, 2026

blake-farman added 7 commits January 11, 2026 09:54

refactor(RingTheory/Ideal/Colon): rename colon_top to colon_univ

19ea59b

refactor(RingTheory/Ideal/Colon): remove Ideal assumption in Ideal.le…

cb28f8d

…_colon

refactor(RingTheory/Ideal/Colon): rename iInf_colon_iSup to iInf_colo…

bc1d874

…n_iUnion

refactor(RingTheory/Ideal/Colon): Renamed colon_eq_top_of_le to colon…

91d0082

…_eq_top_of_subset

refactor(RingTheory/Ideal/Colon): rename colon_inf_eq_left_of_le; ada…

de4207a

…pt proof to iUnion

refactor(RingTheory/Ideal/Colon): add colon_span and simplify mem_col…

c3d46ef

…on_span_singleton

Merge remote-tracking branch 'upstream/master' into colon-generalization

7e6b5c5

github-actions bot removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 11, 2026

erdOne reviewed Jan 12, 2026

View reviewed changes

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 12, 2026

blake-farman added 5 commits January 12, 2026 10:52

refactor(RingTheory/Ideal/Colon): replace deprecated lemma with alias

eff6a71

refactor(RingTheory/Ideal/Colon): replace deprecated iInf_colon_iSup …

8686256

…with alias

refactor(RingTheory/Ideal/Colon): rename colon_bot lemmas and fix simpNF

43b9b32

refactor(RingTheory/Ideal/Colon): split colon_mono into directional l…

e226dcc

…emmas

refactor(RingTheory/Ideal/Colon): rename mem_colon_singleton_set to m…

6c928a9

…em_colon_singleton

blake-farman added 3 commits January 15, 2026 08:29

fix(RingTheory/Ideal/Colon): disable deprecated colon_bot aliases

66e0e4c

refactor(RingTheory/Ideal/Colon): remove deprecated aliases and tidy …

91adac8

…unused declarations

refactor(RingTheory/Ideal/Colon): deprecate mem_colon'

78a08b1

tb65536 approved these changes Jan 15, 2026

View reviewed changes

Mathlib/RingTheory/Ideal/Colon.lean Show resolved Hide resolved

Mathlib/RingTheory/Ideal/Colon.lean Outdated Show resolved Hide resolved

Mathlib/RingTheory/Ideal/Colon.lean Outdated Show resolved Hide resolved

blake-farman added 3 commits January 15, 2026 10:11

fix(RingTheory/Ideal/Colon): restore deprecated alias colon_bot

aace54b

style(RingTheory/Ideal/Colon): simplify Set.univ binder in colon_univ

6ab89f3

refactor(RingTheory/Ideal/Colon): simplify Ideal.le_colon proof

bf4028b

erdOne reviewed Jan 15, 2026

View reviewed changes

Mathlib/RingTheory/Lasker.lean Outdated Show resolved Hide resolved

erdOne reviewed Jan 15, 2026

View reviewed changes

Mathlib/RingTheory/Ideal/Colon.lean Outdated Show resolved Hide resolved

erdOne approved these changes Jan 15, 2026

View reviewed changes

leanprover-community-mathlib4-bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 15, 2026

blake-farman added 2 commits January 15, 2026 17:53

refactor(RingTheory/Lasker): simplify colon calculation in InfIrred.i…

0b19437

…sPrimary

doc(RingTheory/Ideal/Colon): note colon naming convention.

1cdbd41

leanprover-community-mathlib4-bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 16, 2026

mathlib-bors bot changed the title ~~feat(RingTheory/Ideal): generalize Submodule.colon to sets~~ [Merged by Bors] - feat(RingTheory/Ideal): generalize Submodule.colon to sets Jan 16, 2026

mathlib-bors bot closed this Jan 16, 2026

adomani mentioned this pull request Jan 16, 2026

feat: MiM PR report #15355

Open

farmanb pushed a commit to farmanb/mathlib4 that referenced this pull request Jan 16, 2026

refactor(RingTheory/IdealFilter/Basic): use generalized colon API

837e31d

This adapts IdealFilter to the generalized Submodule.colon API introduced in leanprover-community#33390.

[Merged by Bors] - feat(RingTheory/Ideal): generalize Submodule.colon to sets #33390

[Merged by Bors] - feat(RingTheory/Ideal): generalize Submodule.colon to sets #33390

Uh oh!

Conversation

farmanb commented Dec 29, 2025

Uh oh!

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

Uh oh!

PR summary 19e41d0839

Import changes for modified files

Declarations diff

Uh oh!

farmanb commented Jan 8, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

erdOne commented Jan 10, 2026

Uh oh!

farmanb commented Jan 11, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

erdOne left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jan 15, 2026

Uh oh!

riccardobrasca commented Jan 16, 2026

Uh oh!

mathlib-bors bot commented Jan 16, 2026

Uh oh!

farmanb commented Jan 16, 2026

Uh oh!

mathlib-bors bot commented Jan 16, 2026

Uh oh!

mathlib-bors bot commented Jan 16, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented Dec 29, 2025 •

edited

Loading