Skip to content

feat(Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum#23320

Closed
Whysoserioushah wants to merge 14 commits intomasterfrom
span'
Closed

feat(Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum#23320
Whysoserioushah wants to merge 14 commits intomasterfrom
span'

Conversation

@Whysoserioushah
Copy link
Copy Markdown
Collaborator

@Whysoserioushah Whysoserioushah commented Mar 25, 2025 •
edited by grunweg
Loading

co-authored by: @jjaassoonn

splited from #23216 following @eric-wieser advice

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 25, 2025 •
edited
Loading

PR summary a40dba502b

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.RingTheory.TwoSidedIdeal.SpanAsSum (new file) 1248

Declarations diff

+ mem_span_ideal_iff_exists_fin
+ mem_span_iff_exists_fin
+ mem_span_range_iff_exists_multisetSum

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 github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Mar 25, 2025
eric-wieser
eric-wieser reviewed Mar 26, 2025
View reviewed changes
kbuzzard
kbuzzard reviewed Mar 27, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Mar 31, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Mar 31, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Mar 31, 2025
View reviewed changes
eric-wieser
eric-wieser reviewed Mar 31, 2025
View reviewed changes
Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum.lean
Comment on lines +62 to +64
lemma mem_span_range_iff_exists_multisetSum (ι : Type*) (v : ι → R) (x : R) :
x ∈ span (Set.range v) ↔ ∃ l : Multiset (R × ι × R),
(l.map fun | (l, i, r) => l * v i * r).sum = x := by
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser Mar 31, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@j-loreaux, can you think of a nice statement of this that makes sense for non-unital rings? Perhaps a Multiset (WithOne R × ι × WithOne R) along with a DistribMulAction (WithOne R) R instance for NonUnitalRing R?

eric-wieser
eric-wieser reviewed Mar 31, 2025
View reviewed changes
@Paul-Lez Paul-Lez self-requested a review April 3, 2025 14:02
Paul-Lez
Paul-Lez reviewed Apr 3, 2025
View reviewed changes
Whysoserioushah and others added 2 commits April 3, 2025 16:05
@Whysoserioushah @Paul-Lez
Update Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
8350a89 
Co-authored-by: Paul Lezeau <paul.lezeau@gmail.com>
@Whysoserioushah
revert
86d0261
@Whysoserioushah Whysoserioushah requested a review from b-mehta April 3, 2025 19:24
eric-wieser
eric-wieser reviewed Apr 8, 2025
View reviewed changes
@eric-wieser eric-wieser mentioned this pull request Apr 8, 2025
Closed
2 tasks
@Whysoserioushah Whysoserioushah mentioned this pull request Apr 8, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Apr 8, 2025
@Whysoserioushah @eric-wieser
chore(RingTheory/TwoSidedIdeal/Operations): Add span_induction (#23850)
ca643a5 
splitted from #23320 following @eric-wieser advice
Co-authored-by: Jujian Zhang <jujian.zhang19@imperial.ac.uk>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
eric-wieser
eric-wieser reviewed May 9, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's ultimately not clear to me that this PR is useful, given that we already have TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure from #14460 (cc @jjaassoonn, @j-loreaux)

@Whysoserioushah
Copy link
Copy Markdown
Collaborator Author

Whysoserioushah commented May 9, 2025

It's ultimately not clear to me that this PR is useful, given that we already have TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure from #14460 (cc @jjaassoonn, @j-loreaux)

this was used to prove wedderburn but since @alreadydone already has several PRs to prove that I would say it's not urgently needed but I'm still going to need this theorem at some point later, when I get there if this PR is still not merged I could make another dependent PR to convince you :)

tannerduve pushed a commit that referenced this pull request May 13, 2025
@Whysoserioushah @eric-wieser @tannerduve
chore(RingTheory/TwoSidedIdeal/Operations): Add span_induction (#23850)
85550ec 
splitted from #23320 following @eric-wieser advice
Co-authored-by: Jujian Zhang <jujian.zhang19@imperial.ac.uk>



Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@Whysoserioushah
Copy link
Copy Markdown
Collaborator Author

Whysoserioushah commented Jun 23, 2025

I will close this PR and make a new one from my fork

@Whysoserioushah Whysoserioushah mentioned this pull request Jul 3, 2025
Open
@YaelDillies YaelDillies deleted the span' branch August 1, 2025 06:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@kbuzzard kbuzzard kbuzzard left review comments

@erdOne erdOne Awaiting requested review from erdOne

@b-mehta b-mehta Awaiting requested review from b-mehta

+1 more reviewer

@Paul-Lez Paul-Lez Paul-Lez left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

@eric-wieser eric-wieser

Labels

t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@Whysoserioushah @eric-wieser @kbuzzard @Paul-Lez