feat (group_theory/amenable) : Finite groups are amenable #16695
matthias567
wants to merge
18 commits into
master
from
amenable_groups-fin
feat (group_theory/amenable) : define amenable groups
a5314494
feat (group_theory/amenable) : Finite groups are amenable.
b7a63e49
fix authors (s missing)
2b096c84
rm superfluous aux_lemma_sums
6879c71d
mean: switch to topological groups
1d9f3c89
def_amenable: swith to topological_groups
c86d4b2d
finite_groups: rewrite proof for topological groups
9da273b0
Merge remote-tracking branch 'origin/master' into amenable_groups
17ca6e6d
rm finite_groups (will be a different PR to make the PR smaller)
9720321c
adapt to structure guidlines : structure def and theorems
cf836ce0
doc guidelines
979f274c
feat (group_theory/amenable) : Finite groups are amenable
493e9838
classical.some -> classical.choice
1b477289
.mk -> constructor notation
143c99ae
feat (group_theory/amenable) : Finite groups are amenable
d92be715
Merge branch 'amenable_groups-fin' of github.com:leanprover-community…
2c5de555
adapt to style guidelines
d440110d
add noncomputable
c84383db
Reviewers
No reviews
Assignees
No one assigned
Labels
awaiting-review
blocked-by-other-PR
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub