leanprover-community/mathlib3

Pull Requests Commits

Make it non-assoc

mans0954 committed 2 years ago

44d5d14d

Merge branch 'non-assoc-star-mul' into centroid_star

mans0954 committed 2 years ago

18038273

rename star_semigroup star_magma

mans0954 committed 2 years ago

ca9d6c5e

Merge branch 'non-assoc-star-mul' into centroid_star

mans0954 committed 2 years ago

1a89952f

Take coe_pow out of simp

mans0954 committed 2 years ago

56f47732

Merge branch 'master' into non-assoc-star-mul

mans0954 committed 2 years ago

9e6803a4

feat(analysis/convolution): regularity of convolution for functions depending on a parameter (#17626)

sgouezel committed 2 years ago

9d81ef7e

feat(probability/kernel/basic): measurability of the integral against a kernel (#18061)

RemyDegenne committed 2 years ago

2bb0d084

feat(data/real/ennreal): `mul_div_mul_left` (#18051)

madvorak committed 2 years ago

ad1c83e8

feat(combinatorics/simple_graph/connectivity): `walk.to_subgraph` (#17325)

kmill committed 2 years ago

d6e84a0d

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

leanprover-community-bot committed 2 years ago

10708587

chore(algebra/continued_fractions): golf some proofs (#18082)

urkud committed 2 years ago

134625f5

feat(analysis/convex): add lemma for composition of convex functions (#15111)

ericluap committed 2 years ago

14e84382

chore({ring_theory, field_theory}/*): fix imports to make #18021 less messy (#18065)

Paul-Lez committed 2 years ago

3e00d81b

feat(data/set/finite): Align `set.to_finset` and `set.finite.to_finset` (#17959)

YaelDillies committed 2 years ago

117e93f8

feat(data/set/function): `∘` lemmas (#17819)

YaelDillies committed 2 years ago

67f36267

feat(geometry/manifold/cont_mdiff): generalize some lemmas to arbitrary charts (#17668)

fpvandoorn committed 2 years ago

e6444585

chore(analysis/normed_space/lp_equiv): fix docs (#18073)

ericrbg committed 2 years ago

6afc9b06

chore(algebra/continued_fractions): golf 2 proofs (#18070)

urkud committed 2 years ago

c85b4d15

feat(ring_theory/polynomial/cyclotomic/eval): golf, add lemmas (#18022)

urkud committed 2 years ago

55d224c3

feat(order/lattice): `a ⊔ b = a ⊓ b ↔ a = b` (#17966)

YaelDillies committed 2 years ago

d6aad952

feat(logic/function/iterate): Cancelling iterates (#17956)

YaelDillies committed 2 years ago

792a2a26

feat(group_theory/perm/basic): `mul_left` is a monoid hom (#17900)

YaelDillies committed 2 years ago

730513c7

feat(analysis/bounded_variation): lower semicontinuity of `variation_on` (#18058)

bottine committed 2 years ago

2ed7e4ae

feat(data/int/cast/lemmas): `a.nat_mod b < b` (#17896)

YaelDillies committed 2 years ago

7a89b1ae

docs(data/nat/choose/sum): binomial theorem is for commuting elements (#18071)

madvorak committed 2 years ago

18a5306c

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

leanprover-community-bot committed 2 years ago

00f4ab49

feat(data/list/infix): `list.slice` is a sublist of the original (#18067)

eric-wieser committed 2 years ago

26f081a2

chore(data/{int,nat}/modeq): Rationalise lemma names (#17902)

YaelDillies committed 2 years ago

c0dbeca1

feat(topology/order/basic): replace `partial_order` by `preorder` (#18064)

alreadydone committed 2 years ago

ed005a8c

Older