leanprover-community/mathlib

Pull Requests Commits

kex-y committed 3 years ago

f0fa5a5f

Lévy's Borel-Cantelli sorry free

kex-y committed 3 years ago

cd80e2c5

kex-y committed 3 years ago

aacfc764

clear some sorries

kex-y committed 3 years ago

e3b310fe

kex-y committed 3 years ago

da7aad61

kex-y committed 3 years ago

d06f5171

difference bounded

kex-y committed 3 years ago

3d454f31

mgale is martingale

kex-y committed 3 years ago

7cb3d014

Merge branch 'master' of https://github.com/leanprover-community/mathlib into JasonKYi/upcrossing_spec

kex-y committed 3 years ago

3c07dc56

chore(probability/martingale): add some parity lemmas for martingales and supermartingales (#15811)

kex-y committed 3 years ago

777082da

kex-y committed 3 years ago

a632702c

feat(algebra/big_operators/multiset): add `prod_map_erase` for `list` and `multiset` (#15808)

astrainfinita committed 3 years ago

bedd9506

feat(geometry/manifold/mfderiv): differentiability is a `local_invariant_prop`, and consequences (#15666)

hrmacbeth committed 3 years ago

58004685

feat(algebraic_geometry/EllipticCurve): add 2-torsion polynomials and changes of variables (#15230)

Multramate committed 3 years ago

c06c6806

feat(number_theory/legendre_symbol/gauss_sum): add file gauss_sum.lean (#15684)

MichaelStollBayreuth committed 3 years ago

2a2d33c8

feat(ring_theory/dedekind_domain): promote fractional ideals to `semifield` (#15794)

Vierkantor committed 3 years ago

aafeb5f3

add some lemmas

kex-y committed 3 years ago

0d96745c

kex-y committed 3 years ago

cdd30c5e

kex-y committed 3 years ago

f8e11efb

chore(*): golf using new `positivity` tactic (#15701)

hrmacbeth committed 3 years ago

5bd49e4c

feat(algebra/algebra/bilinear): make `algebra.lmul` to apply to non-unital (non-assoc) algebras (#15310)

j-loreaux committed 3 years ago

9264b15e

lemmas about coeff for `compute_degree` (#15694)

adomani committed 3 years ago

10a5ded3

prove the aux lemmas

kex-y committed 3 years ago

631d68ca

fix(algebra/monoid_algebra/basic): add `int_cast` to `monoid_algebra` instances (#15779)

ericrbg committed 3 years ago

59874523

fix(tactic/rcases): support `rcases x with y` renames (#15773)

digama0 committed 3 years ago

073a3e97

refactor(category_theory): custom structure for full_subcategory (#14767)

TwoFX committed 3 years ago

bb103f35

kex-y committed 3 years ago

305eed38

feat(order/rel_iso): relation embeddings for `sum.lex` and `prod.lex` (#15355)

vihdzp committed 3 years ago

7200c507

feat(geometry/euclidean/oriented_angle): relation to unoriented angles (#15722)

jsm28 committed 3 years ago

674505ed

feat(algebra/order/floor): `fract_one` (#15785)

jsm28 committed 3 years ago

7dcf5c3d

Older