leanprover-community/mathlib3

Pull Requests Commits

Merge branch 'sup2' into sup3

kim-em committed 3 years ago

b371e855

kim-em committed 3 years ago

ec3bcf93

refactor(*): supremum of several recent refactoring PRs (#17381)

kim-em committed 3 years ago

f7707875

some fixes that should have been in #17381

kim-em committed 3 years ago

88e8f1d2

fix downstream imports

kim-em committed 3 years ago

4a0cae5b

feat(group_theory/*): Add `finite` instances (#17377)

tb65536 committed 3 years ago

34fa1f81

chore(data/finset/prod): golf a proof (#17373)

eric-wieser committed 3 years ago

382bdab6

chore(data/nat/cast): remove spurious imports (#17336)

kim-em committed 3 years ago

ed04b515

chore(category_theory): better definitional properties for kernel_lift (#17328)

joelriou committed 3 years ago

4dabfb92

feat(combinatorics/simple_graph/connectivity): Transfer walks from a `simple_graph` to another (#17326)

bottine committed 3 years ago

7a5f20f4

feat(category_theory/limits/shapes/binary_products): API for binary (co)products (#17317)

erdOne committed 3 years ago

fec1d95f

feat(src/topology/category/Top/limits): Coproducts in `Top`. (#17282)

erdOne committed 3 years ago

480c757a

feat(data/{seq,stream}): enum and some helper API (#15790)

pechersky committed 3 years ago

22f02c16

kim-em committed 3 years ago

bda37667

Merge branch 'sup' into sup2

kim-em committed 3 years ago

b607dbfd

kim-em committed 3 years ago

b1b9fd9e

kim-em committed 3 years ago

e6d08250

kim-em committed 3 years ago

946f2928

refactor(data/rat/defs): split

kim-em committed 3 years ago

79a938bc

chore(combinatorics/set_family/intersecting): extract a repeated proof into a lemma (#17371)

eric-wieser committed 3 years ago

c5e13bd0

feat(data/fintype/basic): add missing bounded_order instance for finset (#17370)

eric-wieser committed 3 years ago

f3586f28

chore(analysis/normed_space/bounded_linear_maps): squeeze simps (#17368)

mcdoll committed 3 years ago

a9a490da

chore(linear_algebra/basic): squeeze non-terminal simps (#17367)

mcdoll committed 3 years ago

4bb16a67

chore(data/finsupp/basic): golf a lemma (#17366)

eric-wieser committed 3 years ago

654bbd9c

chore(linear_algebra/basic): add `linear_equiv.conj_apply_apply` (#17364)

eric-wieser committed 3 years ago

fbaa3ad0

chore(data/finsupp): move and rename `finsupp.single_apply_left` (#17357)

Vierkantor committed 3 years ago

34fb08a7

split(algebra/order/nonneg): Separate `ring` and `field` instances (#17348)

YaelDillies committed 3 years ago

43e01caf

can't resist one more

kim-em committed 3 years ago

c089f012

kim-em committed 3 years ago

edcbcecc

Merge branch 'pairwise' into sup

kim-em committed 3 years ago

1e81f661

Older