leanprover-community/mathlib

Pull Requests Commits

TwoFX committed 3 years ago

1595f109

refactor(topology/separation): redefine `t0_space` (#15046)

urkud committed 3 years ago

d45a8ace

feat(analysis/inner_product_space): add simple lemmas for the orthogonal complement (#15020)

mcdoll committed 3 years ago

71b1be63

feat(geometry/manifold/local_invariant_properties): simplify definitions and proofs (#15116)

fpvandoorn committed 3 years ago

f09322bc

feat(analysis/special_functions/complex/arg): add complex.abs_eq_one_iff (#15125)

Ruben-VandeVelde committed 3 years ago

8ff5e113

chore(data/fintype): drop a `decidable_pred` assumption (#14971)

urkud committed 3 years ago

d908bc0b

feat(probability/martingale): Doob's maximal inequality (#14737)

kex-y committed 3 years ago

a95b4427

doc(overview): add probability theory (#15114)

fpvandoorn committed 3 years ago

bd9c307d

feat(analysis/convex/function): Variants of `convex_on.le_right_of_left_le` (#14821)

tb65536 committed 3 years ago

93e97d1e

chore(analysis/normed/field/basic): add `@[simp]` to `real.norm_eq_abs (#15006)

urkud committed 3 years ago

71e11de8

feat(probability/martingale): positive part of a submartingale is also a submartingale (#14932)

kex-y committed 3 years ago

071dc908

feat(*): add lemmas about sigma types (#15085)

urkud committed 3 years ago

f10d0abc

feat(topology/sets/compacts): prod constructions (#15118)

sgouezel committed 3 years ago

527afb3d

feat(analysis/complex): equiv_real_prod_symm_apply (#15122)

sgouezel committed 3 years ago

db9cb466

feat(measure_theory/group/measure): a product of Haar measures is a Haar measure (#15120)

sgouezel committed 3 years ago

68ae182e

chore(data/set/*,order/*): add missing lemmas about `monotone_on` etc (#14943)

urkud committed 3 years ago

365e30de

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

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

feat(data/nat/basic): add `mul_div_mul_comm_of_dvd_dvd` (#15031)

stuart-presnell committed 3 years ago

4823da23

Older