leanprover-community/mathlib

Pull Requests Commits
feat(measure_theory/group/measure): a product of Haar measures is a Haar measure (#15120)
sgouezel committed 3 years ago
68ae182e
no sorry left
RemyDegenne committed 3 years ago
aff1b5ba
Merge remote-tracking branch 'origin/RD_chernoff_bound' into RD_subgaussian
RemyDegenne committed 3 years ago
2a612356
copy
RemyDegenne committed 3 years ago
98eff175
Merge remote-tracking branch 'origin/RD_indep_comp' into RD_subgaussian
RemyDegenne committed 3 years ago
ae0382c0
make variables implicit
RemyDegenne committed 3 years ago
be37190d
spaces
RemyDegenne committed 3 years ago
b1d4ab74
docstrings
RemyDegenne committed 3 years ago
616bd056
fix
RemyDegenne committed 3 years ago
d0e12f91
chore(data/set/*,order/*): add missing lemmas about `monotone_on` etc (#14943)
urkud committed 3 years ago
365e30de
expand docstring
RemyDegenne committed 3 years ago
1e37849c
docstrings
RemyDegenne committed 3 years ago
fff66bc1
change names
RemyDegenne committed 3 years ago
a5a6793e
move a lemma
RemyDegenne committed 3 years ago
0c6f4a4c
independence of joint r.v.
RemyDegenne committed 3 years ago
f54cae01
feat(measure_theory/function/conditional_expectation): monotonicity of the conditional expectation (#15024)
kex-y committed 3 years ago
dba3dcef
refactor(analysis/convex/specific_functions): Remove hypothesis from `deriv_sqrt_mul_log` (#15015)
tb65536 committed 3 years ago
676e7725
refactor(data/real/ennreal): golf, generalize (#14996)
urkud committed 3 years ago
83eda07e
add left tail versions
RemyDegenne committed 3 years ago
79b7bd6d
add chernoff bound
RemyDegenne committed 3 years ago
328544aa
chore(analysis/calculus/deriv): make the exponent explicit in pow lemmas (#15117)
sgouezel committed 3 years ago
18860933
feat(number_theory/wilson): add Wilson's Theorem (#14717)
jn1z committed 3 years ago
73d15d77
feat(analysis/special_functions/complex/arg): `continuous_at_arg_coe_angle` (#14980)
jsm28 committed 3 years ago
06ac34b8
feat(geometry/euclidean/basic): `continuous_at_angle` (#15021)
jsm28 committed 3 years ago
8f391f56
chore(ring_theory/matrix_algebra): golf using `matrix.map` (#15040)
eric-wieser committed 3 years ago
407f39b0
refactor(data/nat/parity): `nat.even_succ` -> `nat.even_add_one` (#14917)
BoltonBailey committed 3 years ago
051dffa5
feat(category_theory/limits): bilimit from kernel (#14452)
TwoFX committed 3 years ago
46344b4d
refactor(category_theory): generalise universe levels in preservation statements (#15067)
javra committed 3 years ago
024a4231
chore(ring_theory/dedekind_domain/ideal): fix style of a lemma statement (#15097)
Paul-Lez committed 3 years ago
6e8f25e1
feat(ring_theory/dedekind_domain): If `R/I` is isomorphic to `S/J` then the factorisations of `I` and `J` have the same shape (#11053)
Paul-Lez committed 3 years ago
9e701b98
Terms Of Use Privacy Policy Refund Policy Impressum