leanprover-community/mathlib

Pull Requests Commits

feat(algebra/group/opposite): `is_unit` lemmas for `mul_opposite` (#19080)

eric-wieser committed 2 years ago

0372d31f

eric-wieser committed 2 years ago

1c7f6abb

eric-wieser committed 2 years ago

192b64a9

Merge remote-tracking branch 'origin/master' into eric-wieser/lp_space-bounded

eric-wieser committed 2 years ago

71296cb4

elaboration help

eric-wieser committed 2 years ago

04cc2f5f

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

riccardobrasca committed 2 years ago

5bfbcca0

missing instance

eric-wieser committed 2 years ago

25b45091

eric-wieser committed 2 years ago

61faa89c

refactor(measure_theory/function/lp_space): generalize actions from `normed_field` to `normed_ring`

eric-wieser committed 2 years ago

cb4e848f

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

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

leanprover-community-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

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

feat: update to Lean 3.51.0 (#19060)

eric-wieser committed 2 years ago

05b93a58

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

leanprover-community-bot committed 2 years ago

cb9077f7

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

leanprover-community-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

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

eric-wieser committed 2 years ago

75e7fca5

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

feat(probability/kernel/disintegration): disintegration of finite measures on product spaces (#18834)

RemyDegenne committed 2 years ago

3b88f400

chore(linear_algebra/basis): `simp` lemmas about `basis.equiv_fun` (#19021)

eric-wieser committed 2 years ago

13bce9a6

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

leanprover-community-bot committed 2 years ago

4280f5f3

feat(combinatorics/simple_graph): Szemerédi's Regularity Lemma (#11000)

YaelDillies committed 2 years ago

1d4d3ca5

Newer Older