mathlib3
feat(ring_theory): Wedderburn's little theorem (finite domains are fields)
#9856

Open

feat(ring_theory): Wedderburn's little theorem (finite domains are fields) #9856

jcommelin wants to merge 56 commits into master from little-wedderburn

feat(ring_theory/integral_domain): finite domains are division rings

802b23bb

class equation

3c7f67c2

Merge branch 'finite-domain' into little-wedderburn

e334f375

start towards little wedderburn

d4a0dfa6

wip

433a8794

Merge branch 'master' into little-wedderburn

4a2aedfc

wip

83bfa66f

Merge branch 'master' into little-wedderburn

29096507

wip

c9f19b99

sorry-free

f06f1560

jcommelin added WIP

Vierkantor commented on 2021-10-21

riccardobrasca commented on 2021-10-21

ADedecker commented on 2021-10-22

eric-wieser commented on 2021-10-23

github-actions added blocked-by-other-PR

github-actions added merge-conflict

github-actions removed blocked-by-other-PR

Merge branch 'master' into little-wedderburn

ea929330

github-actions removed merge-conflict

Resolve merge breakages

b8f3964d

jcommelin added please-adopt

Merge branch 'master' into little-wedderburn

299e5981

quicfix

985cc57c

(lint)fix

9939119d

further tidy

59d58aeb

tidy

32edb198

ericrbg removed please-adopt

leanprover-community-bot-assistant added blocked-by-other-PR

leanprover-community-bot-assistant removed blocked-by-other-PR

leanprover-community deleted a comment from github-actions on 2022-03-02

a lot of changes that I should've commited separately

91779c13

Merge branch 'master' into little-wedderburn

a92763a5

remove theorems

a61b2078

leanprover-community-bot-assistant added blocked-by-other-PR

fixup

e14a13a5

tidy

c4a3ab9d

Merge branch 'master' into little-wedderburn

b6e87029

leanprover-community-bot-assistant removed blocked-by-other-PR

Merge branch 'master' into little-wedderburn

26818992

bump and fix

e1968291

leanprover-community-bot-assistant added blocked-by-other-PR

preliminary tidy, wait for build

bb9d2af8

more fixes

f69882dd

Merge remote-tracking branch 'origin/master' into little-wedderburn

b6cbde79

fintype diamonds :)

dd7e8a4d

actually fix

d8174411

more instances? :/

ce64bdec

more messing with fintypes

45051be9

oops

226bee82

leanprover-community-bot-assistant added merge-conflict

leanprover-community-bot-assistant removed blocked-by-other-PR

Merge remote-tracking branch 'origin/master' into little-wedderburn

1f0aaa9f

leanprover-community-bot-assistant removed merge-conflict

fix

218fa9df

fix

82a4f118

feat(algebra/group/conj): instances + misc

3d6f94bf

Merge branch 'ericrbg/conj_improvements' into little-wedderburn

ebe42c6c

ghost added blocked-by-other-PR

ghost removed blocked-by-other-PR

ghost deleted a comment from leanprover-community-bot-assistant on 2022-05-19

Merge branch 'master' into little-wedderburn

3507f77a

fix

4329d48e

but for real

35132062

Merge remote-tracking branch 'origin/master' into little-wedderburn

31151eac

github-actions added modifies-synchronized-file

Phone github spacing :(

e0589002

small tidy

2aa37629

further tidy

59670560

more tidying

b5f1f503

upgrade centralizer

f40e7f9c

split off

1c383cfc

remove duplicate namespace

d4a9d5d8

remove my multiple namespace hack

7ca63791

Delete centralizer.lean

3b81c0ee

ghost added blocked-by-other-PR

Update little_wedderburn.lean

fb40886d

finite tidy

432ec20b

jcommelin added please-adopt

Merge branch 'master' into little-wedderburn

dc95da58

riccardobrasca commented on 2023-06-08

fix

4a143d67

ghost removed blocked-by-other-PR

Merge remote-tracking branch 'origin/master' into little-wedderburn

20eebc88

kim-em added too-late

Reviewers

ericrbg

riccardobrasca

eric-wieser

ADedecker

Vierkantor

Assignees

No one assigned

Labels

WIP please-adopt modifies-synchronized-file too-late

Milestone

No milestone

mathlib3 feat(ring_theory): Wedderburn's little theorem (finite domains are fields) #9856 Open

feat(ring_theory): Wedderburn's little theorem (finite domains are fields) #9856

mathlib3
feat(ring_theory): Wedderburn's little theorem (finite domains are fields)
#9856

Open