feat(Mathlib/RingTheory/TwoSidedIdeal/WedderburnArtin): Wedderburn-Artin Theorem by Whysoserioushah · Pull Request #23583 · leanprover-community/mathlib4

Whysoserioushah · 2025-04-02T09:55:03Z

Co-authored-by : Jujian Zhang jujian.zhang19@imperial.ac.uk

depends on: feat(Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum #23320
depends on: [Merged by Bors] - chore(RingTheory/TwoSidedIdeal/Operations): Add span_induction #23850

github-actions · 2025-04-02T09:57:38Z

PR summary 8aeb431989

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)	1253
`Mathlib.RingTheory.WedderburnArtin` (new file)	1407

Declarations diff

+ Ideal.eq_of_le_of_isSimpleModule
+ LinearEquiv.conjRingEquiv_apply
+ LinearEquiv.conjRingEquiv_symm_apply
+ TwoSidedIdeal.span_eq_bot
+ Wedderburn_Artin
+ Wedderburn_Artin'
+ Wedderburn_Artin.aux.one_eq
+ Wedderburn_Artin_algebra_version
+ Wedderburn_Artin_algebra_version'
+ Wedderburn_Artin_ideal_version
+ mem_span_ideal_iff_exists_fin
+ mem_span_iff_exists_fin
+ mem_span_range_iff_exists_multisetSum
+ minimal_ideal_isSimpleModule

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.

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
933	1	erw

Current commit 8aeb431989
Reference commit ca643a512c

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

Mathlib/RingTheory/WedderburnArtin.lean

Mathlib/RingTheory/TwoSidedIdeal/Operations.lean

Mathlib/RingTheory/WedderburnArtin.lean

mathlib4-dependent-issues-bot · 2025-04-08T23:21:43Z

This PR/issue depends on:

feat(Mathlib/RingTheory/TwoSidedIdeal/SpanAsSum): span of set as finsum #23320
~~[Merged by Bors] - chore(RingTheory/TwoSidedIdeal/Operations): Add span_induction #23850~~
By Dependent Issues (🤖). Happy coding!

Mathlib/RingTheory/WedderburnArtin.lean

Whysoserioushah · 2025-04-13T14:43:31Z

closing this PR as the content is in #23963

@Whysoserioushah

…23963) A replacement of #23583 with more meaningful intermediate results. Co-authored-by: Edison Xie @Whysoserioushah Co-authored-by: Jujian Zhang [jujian.zhang19@imperial.ac.uk](mailto:jujian.zhang19@imperial.ac.uk)

@Whysoserioushah

…23963) A replacement of #23583 with more meaningful intermediate results. Co-authored-by: Edison Xie @Whysoserioushah Co-authored-by: Jujian Zhang [jujian.zhang19@imperial.ac.uk](mailto:jujian.zhang19@imperial.ac.uk)

@Whysoserioushah

…eanprover-community#23963) A replacement of leanprover-community#23583 with more meaningful intermediate results. Co-authored-by: Edison Xie @Whysoserioushah Co-authored-by: Jujian Zhang [jujian.zhang19@imperial.ac.uk](mailto:jujian.zhang19@imperial.ac.uk)

Whysoserioushah and others added 10 commits March 25, 2025 23:39

create

f4b9b3a

fix comment

b35ec6e

add induction

1bc6fcf

add multiSet

6c5a9b5

remove span'

d7fa9db

eric suggestion 3

0b3889e

eric suggestion 5

3e1fc78

golf and generalize

2876b63

Merge branch 'master' into span'

c631f58

wip

e6827a6

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

fix lint and build

be61d94

Whysoserioushah requested a review from eric-wieser April 2, 2025 10:04

jcommelin reviewed Apr 3, 2025

View reviewed changes

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

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

Mathlib/RingTheory/WedderburnArtin.lean Show resolved Hide resolved

Whysoserioushah added 2 commits April 3, 2025 15:07

del

5572713

fix

ab9ac18

ScottCarnahan reviewed Apr 4, 2025

View reviewed changes

Mathlib/RingTheory/TwoSidedIdeal/Operations.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Apr 4, 2025

View reviewed changes

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

eric-wieser reviewed Apr 4, 2025

View reviewed changes

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

Whysoserioushah added 2 commits April 5, 2025 03:12

Merge branch 'master' into edison/wedderburn_wip

7460df6

clean up

8161e2a

eric-wieser reviewed Apr 8, 2025

View reviewed changes

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

eric-wieser reviewed Apr 8, 2025

View reviewed changes

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

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 8, 2025

eric-wieser reviewed Apr 8, 2025

View reviewed changes

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

Whysoserioushah added 3 commits April 9, 2025 01:49

Merge branch 'master' into edison/wedderburn_wip

267b637

fix and del

e7fe788

golf1

0148ead

delete more and cleanup

7c882cc

eric-wieser reviewed Apr 9, 2025

View reviewed changes

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

fix and del2

48ecdb8

Whysoserioushah marked this pull request as ready for review April 9, 2025 20:17

eric-wieser reviewed Apr 9, 2025

View reviewed changes

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

eric suggestion 3

50c569c

eric-wieser reviewed Apr 10, 2025

View reviewed changes

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

eirc suggestion 4

113c67d

Whysoserioushah requested a review from jcommelin April 11, 2025 01:00

Whysoserioushah added 2 commits April 11, 2025 02:34

eric suggestion5

dda66b3

fix

8aeb431

Whysoserioushah requested review from alreadydone and erdOne April 11, 2025 01:55

Whysoserioushah mentioned this pull request Apr 12, 2025

[Merged by Bors] - feat(RingTheory): isotypic API and simple Wedderburn–Artin existence #23963

Closed

1 task

Whysoserioushah changed the title ~~Edison/wedderburn wip~~ feat(Mathlib/RingTheory/TwoSidedIdeal/WedderburnArtin): Wedderburn-Artin Theorem Apr 13, 2025

Whysoserioushah closed this Apr 13, 2025

YaelDillies deleted the edison/wedderburn_wip branch August 15, 2025 16:39

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Mathlib/RingTheory/TwoSidedIdeal/WedderburnArtin): Wedderburn-Artin Theorem#23583

feat(Mathlib/RingTheory/TwoSidedIdeal/WedderburnArtin): Wedderburn-Artin Theorem#23583
Whysoserioushah wants to merge 24 commits intomasterfrom
edison/wedderburn_wip

Whysoserioushah commented Apr 2, 2025 •

edited by github-actions bot

Loading

Uh oh!

github-actions bot commented Apr 2, 2025 •

edited

Loading

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Apr 8, 2025 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Whysoserioushah commented Apr 13, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 8aeb431989

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

mathlib4-dependent-issues-bot commented Apr 8, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Whysoserioushah commented Apr 13, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

Whysoserioushah commented Apr 2, 2025 •

edited by github-actions bot

Loading

github-actions bot commented Apr 2, 2025 •

edited

Loading

mathlib4-dependent-issues-bot commented Apr 8, 2025 •

edited

Loading