leanprover-community/mathlib3

Pull Requests Commits

chore(data/nat): rename oddly named lemma odd_gt_zero (#13040)

alexjbest committed 3 years ago

ab99fd1b

feat(order/lattice, order/lattice_intervals): coe inf/sup lemmas (#15136)

apnelson1 committed 3 years ago

6d02dac3

feat(combinatorics/simple_graph/basic): `dart.to_prod` is injective (#15150)

kmill committed 3 years ago

418373e8

feat(data/quot): `is_equiv` instance for quotient equivalence (#15148)

vihdzp committed 3 years ago

3e52000c

feat(order/rel_iso): add `rel_iso.cast` (#15144)

vihdzp committed 3 years ago

e034eb09

refactor(group_theory/congruence): use `quotient.map` (#15130)

urkud committed 3 years ago

e335a41f

feat(measure_theory/integral): Circle integral transform (#13885)

CBirkbeck committed 3 years ago

fdfc2229

chore(set_theory/ordinal/basic): clean up `ordinal.card` API (#15147)

vihdzp committed 3 years ago

0a89f18f

feat(set_theory/ordinal/basic): basic lemmas on `ordinal.lift` (#15146)

vihdzp committed 3 years ago

a54e63da

feat(order/basic): a symmetric relation implies equality when it implies less-equal (#15149)

vihdzp committed 3 years ago

b7581040

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

Newer Older