leanprover-community/mathlib3

Pull Requests Commits

remove unused lemmas

RemyDegenne committed 2 years ago

21f7ff12

generalize and move borel_eq... lemmas

RemyDegenne committed 2 years ago

09540cb3

Merge remote-tracking branch 'origin/master' into RD_disintegration

RemyDegenne committed 2 years ago

b1a9dda8

Merge remote-tracking branch 'origin/RD_measurable_integral' into RD_integral_kernel

RemyDegenne committed 2 years ago

8ea6f27e

RemyDegenne committed 2 years ago

7112d4b9

RemyDegenne committed 2 years ago

8fbf3c97

place measurable lemmas in the right namespace

RemyDegenne committed 2 years ago

068ecaee

RemyDegenne committed 2 years ago

1fa5be73

remove an intro

RemyDegenne committed 2 years ago

193cb5fd

add set_integral variant

RemyDegenne committed 2 years ago

b9741cc4

RemyDegenne committed 2 years ago

68f920d1

chore(*): add mathlib4 synchronization comments (#18966)

github-actions[bot] committed 2 years ago

7d34004e

feat(*): generalise+add algebraic instances (#18947)

ericrbg committed 2 years ago

949dc57e

feat(data/real/ennreal): interactions between infi/supr and to_nnreal/to_real (#18946)

collares committed 2 years ago

c1686dff

feat(field_theory/adjoin,normal): `field_range` lemmas (#18959)

tb65536 committed 2 years ago

d4437c68

feat(field_theory/intermediate_field): Inhabited instance (#18956)

tb65536 committed 2 years ago

c596622f

RemyDegenne committed 2 years ago

c9378401

Merge remote-tracking branch 'origin/master' into RD_disintegration

RemyDegenne committed 2 years ago

785ca06b

Merge remote-tracking branch 'origin/master' into RD_integral_kernel

RemyDegenne committed 2 years ago

dfe66079

feat(probability/kernel/basic): integrals of basic kernels (#18961)

RemyDegenne committed 2 years ago

a9545e8a

feat(probability/kernel/basic): add `kernel.comap_right` and `kernel.piecewise` (#18917)

RemyDegenne committed 2 years ago

63decdb8

feat(algebra/order/group/order_iso): add `order_iso.div_{left,right}` (#18968)

urkud committed 2 years ago

6632ca20

feat(analysis/calculus/deriv): `polynomial.aeval` lemmas (#18945)

eric-wieser committed 2 years ago

f81174bd

feat(order/category): Category of finite distributive lattices (#11677)

YaelDillies committed 2 years ago

937b1c59

refactor(data/is_R_or_C,analysis/inner_product_space): review API (#18919)

urkud committed 2 years ago

3f655f52

refactor(linear_algebra/dual): make `module.dual` reducible (#18963)

urkud committed 2 years ago

b1c01758

feat(measure_theory/measure/stieltjes): add measure_Iic, measure_Ici, measure_univ (#18884)

RemyDegenne committed 2 years ago

08e1d8d4

RemyDegenne committed 2 years ago

d0e525e7

remove duplicate

RemyDegenne committed 2 years ago

9348e955

remvoe merge lines

RemyDegenne committed 2 years ago

80a5ab1f

Newer Older