leanprover-community/mathlib3

Pull Requests Commits

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

RemyDegenne committed 2 years ago

38ec4d21

chore(ring_theory.polynomial.cyclotomic): split file (#19077)

riccardobrasca committed 2 years ago

5bfbcca0

feat(analysis/normed_space/basic): scaling a set scales its diameter, translating it leaves it unchanged (#18990)

eric-wieser committed 2 years ago

bc91ed70

feat(probability/kernel/disintegration): integral against `cond_kernel` (#19066)

RemyDegenne committed 2 years ago

6315581f

measurable -> ae_measurable

RemyDegenne committed 2 years ago

d46fce1b

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

github-actions[bot] committed 2 years ago

61db041a

feat(analysis/calculus): drop unneeded assumptions (#19045)

urkud committed 2 years ago

3a69562d

feat(order/filter/basic): generalize some lemmas from `nhds_within` (#19070)

urkud committed 2 years ago

d4f691b9

feat(topology/homotopy/H_spaces): define H spaces (#16029)

alreadydone committed 2 years ago

8d33f09c

refactor(analysis/normed_space/basic): generalize some results to actions by normed_rings (#19053)

eric-wieser committed 2 years ago

ba5ff5ad

move things around

RemyDegenne committed 2 years ago

5ee194be

chore(number_theory/cyclotomic): tidying (#19067)

ericrbg committed 2 years ago

b602702a

feat(analysis/calculus/fderiv/star): derivative of star in star-modules over a trivial star-ring (#19038)

eric-wieser committed 2 years ago

ad84a13c

feat(probability/kernel/integral_comp_prod): Bochner integral against the composition-product of two kernels (#18976)

RemyDegenne committed 2 years ago

c0d694db

make cond_distrib irreducible

RemyDegenne committed 2 years ago

4f59d27e

move cond_kernel lemmas

RemyDegenne committed 2 years ago

2e698b8b

move, rename, etc.

RemyDegenne committed 2 years ago

286f7330

feat: update to Lean 3.51.0 (#19060)

eric-wieser committed 2 years ago

05b93a58

RemyDegenne committed 2 years ago

91ee1abc

RemyDegenne committed 2 years ago

a2eb8223

move to disintegration

RemyDegenne committed 2 years ago

2f79cdb2

chore(scripts): update nolints.txt (#19065)

leanprover-community-bot committed 2 years ago

cb9077f7

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

github-actions[bot] committed 2 years ago

38df578a

feat(combinatorics/set_family/compression/uv): UV-compressing reduces the size of the shadow (#13149)

YaelDillies committed 2 years ago

6f8ab7de

RemyDegenne committed 2 years ago

c1461811

RemyDegenne committed 2 years ago

52215048

feat(analysis/calculus/mean_value): functions are equal if their derivatives and a point are equal (#19059)

eric-wieser committed 2 years ago

75e7fca5

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

RemyDegenne committed 2 years ago

fb16b82e

chore(analysis/special_functions/non_integrable): split (#19047)

hrmacbeth committed 2 years ago

55ec6e9a

feat(field_theory/splitting_field): fix the diamond (#18857)

ericrbg committed 2 years ago

b353176c

Older