leanprover-community/mathlib3

Pull Requests Commits

101damnations committed 3 years ago

40c09092

101damnations committed 3 years ago

e45cf5d0

feat(probability/moments): Chernoff bound on the upper/lower tail of a real random variable (#15129)

RemyDegenne committed 3 years ago

a8fdd990

feat(probability/independence): two tuples indexed by disjoint subsets of an independent family of r.v. are independent (#15131)

RemyDegenne committed 3 years ago

0039a198

feat(tactic/lint): add a linter for `[fintype _]` assumptions (#15202)

urkud committed 3 years ago

d6d3d61e

feat(tactic/polyrith): a tactic using Sage to solve polynomial equalities with hypotheses (#14878)

dhruvbhatia00 committed 3 years ago

423a8b92

chore(set_theory/game/ordinal): minor golf (#15253)

vihdzp committed 3 years ago

1f3c2c09

doc(set_theory/game/pgame): divide file into sections (#15250)

vihdzp committed 3 years ago

623a658f

feat(representation_theory/monoid_algebra_basis): add some API for `k[G^n]` (#14308)

Amelia Livingston committed 3 years ago

52d4daef

fix(.github/workflows): temporarily increase timeout (#15251)

digama0 committed 3 years ago

00dbc7b2

refactor(data/nat/enat): rename `enat` to `part_enat` (#15235)

urkud committed 3 years ago

201d2c61

feat(order/hom/basic): `order_iso` to `rel_iso (<) (<)` (#15182)

vihdzp committed 3 years ago

44905df5

feat(combinatorics/simple_graph/connectivity): simp confluence (#15153)

kmill committed 3 years ago

0f56b2df

fix(order/basic): fix `subtype.linear_order` (#15056)

urkud committed 3 years ago

9a2e5c8b

feat(category_theory): left-exact functors preserve finite limits (#14026)

javra committed 3 years ago

bbe25d4d

feat(combinatorics/simple_graph/regularity/equitabilise): Equitabilising a partition (#13222)

YaelDillies committed 3 years ago

d3f5adb0

feat(order/modular_lattice): Semimodular lattices (#11602)

YaelDillies committed 3 years ago

888caf7d

refactor(data/finite): move definition to a new file (#15204)

urkud committed 3 years ago

dfcbe856

data/multiset/range): add multiset.coe_range (#15201)

Ruben-VandeVelde committed 3 years ago

aae01cd3

chore(topology/basic): use `finite` in `locally_finite_of_finite` (#15181)

urkud committed 3 years ago

627bd0c2

feat(data/set/finite): add `multiset.finite_to_set` (#15177)

urkud committed 3 years ago

7f837db4

feat(linear_algebra): basis on R × R, and relation between matrices and linear maps in this basis (#15119)

sgouezel committed 3 years ago

ecd5234f

feat(analysis/inner_product_space): the Hellinger-Toeplitz theorem (#15055)

mcdoll committed 3 years ago

611dccaf

chore(topological_space/sober): use `namespace` and `variables`, golf (#15042)

urkud committed 3 years ago

0980bacb

feat(data/set/pointwise): `list` and `multiset` versions of n-ary lemmas (#14928)

eric-wieser committed 3 years ago

902e351c

feat(algebraic_geometry/projective_spectrum): forward direction of homeomorphism between top_space of Proj and top_space of Spec (#13397)

jjaassoonn committed 3 years ago

b7626956

chore(category_theory/adjunction/*): making arguments implicit in adjuction.comp and two small lemmas about mates (#15062)

Julian-Kuelshammer committed 3 years ago

cea27692

chore(algebra/order/ring): Normalize `_left`/`_right` (#14985)

YaelDillies committed 3 years ago

4e19dab9

feat(category_theory/endofunctor/algebra): Define coalgebras over an endofunctor and prove an equivalence (#14834)

Julian-Kuelshammer committed 3 years ago

40fdf72d

feat(category_theory/functor): preserving/reflecting monos/epis (#14829)

TwoFX committed 3 years ago

f7baecbb

Older