mathlib3
feat (group_theory/amenable) : Quotients of amenable groups are amenable
#16575
Open
Open
feat (group_theory/amenable) : Quotients of amenable groups are amenable #16575
matthias567
wants to merge
52 commits into
amenable_groups
from
amenable_groups-quot
feat(topology/algebra/order): a linear order is T₅ (#16540)
236a0af4
feat(algebra/hom/centroid): Introduce the centroid of a (non-unital, …
30553f13
feat(ring_theory/graded_algebra/basic): lemmas about rings graded by …
9936c3df
feat(linear_algebra/affine_space/affine_subspace): `affine_subspace.s…
e2ce3fa0
feat(analysis/seminorm): continuity criterion for seminorms (#16402)
ae9b867e
feat(topology/algebra/mul_action): `add_torsor.connected_space` (#16471)
a6d28ae9
feat(topology/constructions): add/golf lemmas about `sigma` (#16571)
d2057271
feat(algebra/order/hom/basic): `positivity` extension for nonnegative…
aae2a82f
feat (group_theory/amenable) : Quotients of amenable groups are amena…
640d1e87
feat(algebra/field/opposite): Missing instances (#16564)
84b27545
doc(metric_space/basic): modify doc for metric spaces adding pseudo m…
b1539919
feat(data/complex/exponential): `positivity` extension for `real.exp`…
88f41bb0
feat(analysis/convolution): relax typeclasses and add lemma (#16587)
ec5f9adc
feat(data/polynomial/ring_division): move lemmas, add lemmas (#16432)
f4210e94
rm superfluous aux_lemma_sums
6879c71d
feat(probability/martingale/centering): uniqueness of Doob's decompos…
e18fa7b9
mean: switch to topological groups
1d9f3c89
def_amenable: swith to topological_groups
c86d4b2d
finite_groups: rewrite proof for topological groups
9da273b0
feat(geometry/manifold/instances/sphere): the differential of the emb…
69071436
feat(tactic/positivity): Extension for `coe` (#16141)
3dc8592b
refactor(data/set/basic): Remove _eq lemmas (#16572)
951bf1d9
feat(set_theory/game/nim): recursors for left/right nim moves (#15408)
f18afbe9
chore(topology): golf (#16585)
1732f9cf
doc(topology/algebra/filter_basis): modify doc of `add_group_filter_b…
9806b5c3
chore(analysis): golf a few proofs (#16600)
33075a02
chore(tactic/monotonicity/lemmas): Move lemmas to the correct places …
98cbfb45
chore(.github/workflows): `maintainer merge` workflow (#16555)
79a2eb39
chore(topology/basic): rename lemmas (#16598)
39723052
chore(category/endomorphism): remove unneeded ext attribute (#16603)
028afe5d
feat(analysis/special_functions/pow, set_theory/*): `positivity` exte…
53322d0d
feat(topology/subset_properties): an infinite type with cofinite topo…
02022cd6
chore(tactic): typos in docs (#16510)
f89fa08b
feat(analysis/normed_space/affine_isometry): `subtypeₐᵢ` (#16573)
d0507e7b
chore(data/finset/basic): move `disjoint` proofs earlier (#16436)
24b50bfc
feat(order/filter/lift): replace some implications with iffs (#16452)
313f36d4
feat(category_theory/limits/shapes/biproducts): more (co)kernel insta…
249a9c91
feat(group_theory/group_action): define `distrib_smul` and `smul_zero…
8f66240c
doc(group_theory/sylow): update docstring to include card_eq_multipli…
e1783b0f
feat(topology/separation): connected sets in a t1 space are infinite …
8deb2a68
chore(docs): run `bibtool` on `references.bib` (#16606)
01894cc4
feat(algebra/punit_instances): linear_ordered_add_comm_monoid_with_to…
27b90386
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
classical.some -> classical.choice
1b477289
.mk -> constructor notation
143c99ae
feat (group_theory/amenable) : Quotients of amenable groups are amena…
c234c5a9
adapt quotient to top groups
88bd5766
adapt to style guideline
e61b5990
Merge branch 'amenable_groups-quot' of github.com:leanprover-communit…
35b4ab74
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