leanprover-community/mathlib

Pull Requests Commits

yuma-mizuno committed 4 years ago

defa44b6

yuma-mizuno committed 4 years ago

e7f15be5

Cat is a strict category

yuma-mizuno committed 4 years ago

a7a26dcc

Create locally_discrete.lean

yuma-mizuno committed 4 years ago

e6db176b

Squashed commit of the following:

yuma-mizuno committed 4 years ago

0eb40101

yuma-mizuno committed 4 years ago

61cea0d1

yuma-mizuno committed 4 years ago

fc3a7817

add yoneda lemma

yuma-mizuno committed 4 years ago

bcd658f2

yuma-mizuno committed 4 years ago

24fcb2df

add composition of pseudofunctor

yuma-mizuno committed 4 years ago

5d459fd1

yuma-mizuno committed 4 years ago

d6ca7fc3

yuma-mizuno committed 4 years ago

58a9eb72

yuma-mizuno committed 4 years ago

eb76ce78

yuma-mizuno committed 4 years ago

de8d5c4c

yuma-mizuno committed 4 years ago

12615623

feat(order/complete_boolean_algebra): lemmas about binfi (#10852)

b-mehta committed 4 years ago

04779a32

feat(analysis/normed_space/pointwise): more on pointwise operations on sets in normed spaces (#10820)

sgouezel committed 4 years ago

f00007dc

split(data/finset/sigma): Split off `data.finset.basic` (#10957)

YaelDillies committed 4 years ago

e15e015b

feat(data/finset/*): Random lemmas (#10955)

YaelDillies committed 4 years ago

3f164099

split(data/psigma/order): Split off `order.lexicographic` (#10953)

YaelDillies committed 4 years ago

2b9ab3bb

feat(quadratic_form/prod): quadratic forms on product and pi types (#10939)

eric-wieser committed 4 years ago

43159737

feat(group_theory/index): Transitivity of finite relative index. (#10936)

tb65536 committed 4 years ago

c8f0afcd

feat(data/real/ennreal): add monotonicity lemmas for ennreal.to_nnreal (#10556)

kkytola committed 4 years ago

24cefb50

refactor(*): Random lemmas and modifications from the shifting refactor. (#10940)

erdOne committed 4 years ago

c5bb320c

feat(linear_algebra/quadratic_form/basic): `linear_map.comp_quadratic_form` (#10950)

eric-wieser committed 4 years ago

ee25d58a

feat(linear_algebra/eigenspace): the eigenvalues of a linear endomorphism are in its spectrum (#10912)

dupuisf committed 4 years ago

b2e881b9

feat(data/{finset,multiset}/locally_finite): When an `Icc` is a singleton, cardinality generalization (#10925)

YaelDillies committed 4 years ago

12ee59fa

feat(ring_theory/tensor_product): Range of `tensor_product.product_map` (#10882)

tb65536 committed 4 years ago

da07a992

chore(analysis/normed_space/exponential + logic/function/iterate): fix typos in doc-strings (#10968)

adomani committed 4 years ago

dda469d0

chore(*): fix some doc (#10966)

ericrbg committed 4 years ago

7ca68f8e

Older