feat (group_theory/amenable) : define amenable groups #16574
matthias567
wants to merge
17 commits into
master
from
amenable_groups
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
eric-wieser
commented
on 2022-09-23
Merge remote-tracking branch 'origin/master' into amenable_groups
17ca6e6d
eric-wieser
commented
on 2022-09-23
eric-wieser
commented
on 2022-09-23
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
eric-wieser
commented
on 2022-09-29
eric-wieser
commented
on 2022-09-29
classical.some -> classical.choice
1b477289
.mk -> constructor notation
143c99ae
add monotonicity instead of positivity - halfway through
20d6a9dd
change def mean: positivity -> monotonicity
0ace32b7
eric-wieser
commented
on 2022-10-02
switch to mean_class style def
5838b807
adapt mean to mean_class
1c7b6a94
Reviewers
Assignees
No one assigned
Labels
awaiting-review
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub