leanprover-community/mathlib

Pull Requests Commits

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

madvorak committed 3 years ago

18a5306c

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

github-actions[bot] committed 3 years ago

00f4ab49

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

eric-wieser committed 3 years ago

26f081a2

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

YaelDillies committed 3 years ago

c0dbeca1

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

alreadydone committed 3 years ago

ed005a8c

feat(probability/kernel/basic): deterministic and constant kernels, restriction of a kernel (#18060)

RemyDegenne committed 3 years ago

8f9b933b

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

github-actions[bot] committed 3 years ago

baba818b

feat(ring_theory/dedekind_domain/ideal): add more span_singleton lemmas (#18047)

Multramate committed 3 years ago

50088c97

feat(analysis/convolution): weaken topological assumptions (#18012)

sgouezel committed 3 years ago

8a391fa4

feat(data/finsupp/defs): add add_monoid_hom_class versions of map_range (#17738)

Multramate committed 3 years ago

3c71503b

fix(data/finset/basic): correct the name of `finset.range_coe` which does not mention coercions (#18052)

eric-wieser committed 3 years ago

43a289b5

feat(order/filter/basic): put pp_nodot attribute on filter.tendsto (#18062)

sgouezel committed 3 years ago

5a3e8195

refactor(group_theory/perm/cycle/basic): Consolidate API (#17898)

YaelDillies committed 3 years ago

d1723c04

feat(geometry/euclidean/angle/sphere): law of sines, converse of inscribed angles (#17992)

jsm28 committed 3 years ago

6d0adfa7

chore(field_theory/minpoly): Split results from `minpoly.lean` into three files (#18048)

Paul-Lez committed 3 years ago

d3e8e0a0

chore(data/fin/basic): Remove elab_strategy (#18049)

PatrickMassot committed 3 years ago

3387923e

feat(topology/algebra/module/multilinear): add continuous versions of constructions (#18044)

eric-wieser committed 3 years ago

44b58b42

feat(analysis/bounded_variation): remove [nonempty] from comp_anti/mono lemmas + golf (#18037)

alreadydone committed 3 years ago

ce967b52

feat(category_theory/mittag_leffler): Introduce the Mittag-Leffler condition (#17905)

bottine committed 3 years ago

6cb77a8e

chore(algebra/big_operators/basic): generalize `finset.prod_of_empty` (#18045)

eric-wieser committed 3 years ago

ab3a26d5

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

github-actions[bot] committed 3 years ago

c3291da4

chore(analysis/inner_product_space/basic): golf proofs (#18043)

Ruben-VandeVelde committed 3 years ago

2258b40d

chore(number_theory/well_approximable): use nat.primes (#18042)

Ruben-VandeVelde committed 3 years ago

cf73bb22

chore(*): golf (#18028)

urkud committed 3 years ago

16de0889

fix(scripts/add_port_comments): do not add PR numbers to port comments (#18030)

eric-wieser committed 3 years ago

2da281a1

chore(combinatorics/configuration): Generalize universes (#18039)

tb65536 committed 3 years ago

9830a300

chore(ring_theory/dedekind_domain/ideal): remove fractional_ideal in open namespaces (#18033)

Multramate committed 3 years ago

c3442db1

chore(*): remove references to porting PRs (#18031)

eric-wieser committed 3 years ago

448144f7

feat(ring_theory/ideal/basic): add ideal.span_pair lemmas (#18036)

Multramate committed 3 years ago

5456d487

feat(ring_theory/dedekind_domain/ideal): add fractional_ideal.coe_ideal_span_singleton mul_inv and inv_mul lemmas (#18032)

Multramate committed 3 years ago

1e05171a

Newer Older