leanprover-community/mathlib

Pull Requests Commits

feat(set_theory/game/nim): recursors for left/right nim moves (#15408)

vihdzp committed 3 years ago

f18afbe9

refactor(data/set/basic): Remove _eq lemmas (#16572)

linesthatinterlace committed 3 years ago

951bf1d9

feat(tactic/positivity): Extension for `coe` (#16141)

YaelDillies committed 3 years ago

3dc8592b

feat(geometry/manifold/instances/sphere): the differential of the embedding of the sphere into its ambient space (#16466)

hrmacbeth committed 3 years ago

69071436

finite_groups: rewrite proof for topological groups

matthias567 committed 3 years ago

9da273b0

def_amenable: swith to topological_groups

matthias567 committed 3 years ago

c86d4b2d

mean: switch to topological groups

matthias567 committed 3 years ago

1d9f3c89

feat(probability/martingale/centering): uniqueness of Doob's decomposition (#16532)

kex-y committed 3 years ago

e18fa7b9

rm superfluous aux_lemma_sums

matthias567 committed 3 years ago

6879c71d

feat(data/polynomial/ring_division): move lemmas, add lemmas (#16432)

astrainfinita committed 3 years ago

f4210e94

feat(analysis/convolution): relax typeclasses and add lemma (#16587)

fpvandoorn committed 3 years ago

ec5f9adc

feat(data/complex/exponential): `positivity` extension for `real.exp` (#16492)

YaelDillies committed 3 years ago

88f41bb0

doc(metric_space/basic): modify doc for metric spaces adding pseudo metric spaces (#16577)

faenuccio committed 3 years ago

b1539919

feat(algebra/field/opposite): Missing instances (#16564)

YaelDillies committed 3 years ago

84b27545

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(algebra/order/hom/basic): `positivity` extension for nonnegative homs (#16228)

YaelDillies committed 3 years ago

aae2a82f

feat(topology/constructions): add/golf lemmas about `sigma` (#16571)

urkud committed 3 years ago

d2057271

feat(topology/algebra/mul_action): `add_torsor.connected_space` (#16471)

jsm28 committed 3 years ago

a6d28ae9

feat(analysis/seminorm): continuity criterion for seminorms (#16402)

ADedecker committed 3 years ago

ae9b867e

feat(linear_algebra/affine_space/affine_subspace): `affine_subspace.subtype` (#16372)

jsm28 committed 3 years ago

e2ce3fa0

feat(ring_theory/graded_algebra/basic): lemmas about rings graded by canonically ordered monoids (#16083)

jjaassoonn committed 3 years ago

9936c3df

feat(algebra/hom/centroid): Introduce the centroid of a (non-unital, non-associative) semiring (#12746)

YaelDillies committed 3 years ago

30553f13

feat(topology/algebra/order): a linear order is T₅ (#16540)

urkud committed 3 years ago

236a0af4

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

Newer Older