leanprover-community/mathlib

Pull Requests Commits

feat (group_theory/amenable): Free groups are not amenable.

matthias567 committed 3 years ago

b2718d04

feat (group_theory/amenable) : Quotients of amenable groups are amenable.

matthias567 committed 3 years ago

640d1e87

fix authors (s missing)

matthias567 committed 3 years ago

2b096c84

feat (group_theory/amenable) : Finite groups are amenable.

matthias567 committed 3 years ago

b7a63e49

feat (group_theory/amenable) : define amenable groups

matthias567 committed 3 years ago

a5314494

feat(order/bounded_order): distrib_lattice instances for with_top and with_bot (#16569)

eric-wieser committed 3 years ago

a547b3b3

feat(group_theory/coset): Construct the embedding `H ⧸ ⨅ i, f i → Π i, H ⧸ f i` (#16560)

tb65536 committed 3 years ago

a5ed4088

chore(topology/constructions): use `variables` (#16562)

urkud committed 3 years ago

b7cc093e

feat(combinatorics/additive/pluennecke_ruzsa): The Plünnecke-Ruzsa inequality (#15440)

YaelDillies committed 3 years ago

4aab2abc

feat(data/pfun): Product of partial functions (#15389)

YaelDillies committed 3 years ago

744170a9

feat(topology/uniform_space): Every Cauchy sequence over ℕ is totally bounded (#16563)

mcdoll committed 3 years ago

dc680a80

feat(measure_theory/measurable_space): add `prod.measurable_singleton_class` (#16559)

urkud committed 3 years ago

b76d2b40

feat(model_theory/types): Complete types over a theory (#16548)

awainverse committed 3 years ago

95d67152

refactor(data/real/basic): make `⊓` and `⊔` computable on reals (#16463)

eric-wieser committed 3 years ago

560891c4

feat(topology/separation): define `regular_space` (#16360)

urkud committed 3 years ago

0a67ddd4

feat(data/complex/module): get `smul_comm_class ℝ M E` from the one for `ℂ` (#16513)

j-loreaux committed 3 years ago

9019542b

feat(analysis/special_functions/compare_exp): new file (#16543)

urkud committed 3 years ago

ca827bae

feat(model_theory/*): Lemmas about satisfiability (#16546)

awainverse committed 3 years ago

b3951c65

feat(measure_theory/measurable_space): pi has measurable singletons (#16542)

ericrbg committed 3 years ago

9824a558

chore(probability/process): split `probability/stopping.lean` into three files, create `process` folder (#16521)

RemyDegenne committed 3 years ago

c41e1712

feat(data/real/cau_seq): more lemmas about sup and inf (#16553)

eric-wieser committed 3 years ago

eb7d2664

feat(model_theory/satisfiability): Maximally consistent theories (#16547)

awainverse committed 3 years ago

043a74e2

Revert "first attempt (#16557)"

jcommelin committed 3 years ago

5ea93be0

first attempt (#16557)

jcommelin committed 3 years ago

Verified 1ae5da9d

feat(ring_theory/polynomial/symmetric): restore `finset.powerset_len` version of `prod_X_sub_C_coeff` (#16424)

alreadydone committed 3 years ago

d7e97106

feat(topology/instances/ennreal): diameter of intervals (#16556)

sgouezel committed 3 years ago

d742555c

chore(analysis,topology): replace `noncomputable theory` with `noncomputable` (#16552)

eric-wieser committed 3 years ago

3f498b03

feat(group_theory/commutator): Add `commutator_element_self` (#16437)

tb65536 committed 3 years ago

dcf3c6b6

refactor(topology/constructions): golf, add `@[simp]`/`iff` variants (#16539)

urkud committed 3 years ago

499ab570

feat(data/set/intervals/ord_connected): lemmas about `order_dual` etc (#16534)

urkud committed 3 years ago

77fa4dcf

Older