mathlib3
feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion for simplicity
#10253
Open
Open
feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion for simplicity #10253
AntoineChambert-Loir
wants to merge
16 commits into
master
from
iwasawa_lemma
tb65536
commented
on 2021-11-14
eric-wieser
commented
on 2021-11-24
eric-wieser
commented
on 2021-11-24
pechersky
commented
on 2021-11-24
eric-wieser
commented
on 2021-11-24
eric-wieser
commented
on 2021-11-24
feat(group_theory/iwasawa.lean): add a proof of the Iwasawa criterion…
63427df9
style: remove the final #lint
1b0b36f2
style (group_theory/iwasawa.lean): shorten proofs and remove unused s…
86839bc5
style(group_theory/iwasawa.lean): add copyright, remove #print
ab8c6bb3
style(group_theory/iwasawa.lean): put docstring first
83231db5
style: remove some @
d5ef3ac5
style: adjust comment for docstring
5eff16da
style: adjust comment for docstring
5a77a4c8
feat(src/group_theory/specific_groups/alternating.lean): prove that t…
c8651967
style(src/group_theory/iwasawa.lean): put some universal quantifiers …
1157ed05
style(src/group_theory/specific_groups/alternating.lean): remove ugly…
d1ca2d4c
the good files, finally
41f90a43
style: implementing suggestions of Eric Wieser
af23e254
additional corrections which were overlooked in the previous commit
6444a00f
style: shorten a line (>100 chars)
b804f5d3
blocks and primitive actions
74c53f65
alreadydone
changed the title 
Reviewers
Assignees
No one assigned
Labels
bug
awaiting-author
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub