leanprover-community/mathlib

Pull Requests Commits

abhimanyupallavisudhir committed 6 years ago

8f908e7c

abhimanyupallavisudhir committed 6 years ago

5f94bb2a

feat(linear_algebra): dimension of the base field is 1

johoelzl committed 6 years ago

177b5eb0

refactor(src/data/finset): supr/infi as a directed supr/infi of finite inf/sup

johoelzl committed 6 years ago

0f240304

chore(linear_algebra/basic): relate map/comap/ker/range/comp with 0 and smul; use map/comap Galois connection

johoelzl committed 6 years ago

eeed3218

chore(algebra/pi_instances): generalize pi.list/multiset/finset_prod/sum_apply to dependent types

johoelzl committed 6 years ago

e98999ef

refactor(set_theory/cardinal): split up mk_Union_le_mk_sigma, add mk_Union_eq_mk_sigma; add equiv congruence for subtype

johoelzl committed 6 years ago

ad7ef864

feat(data/{list/alist,finmap}): implicit key type (#662)

spl committed 6 years ago

8a1de249

feat(analysis/metric_space): Isometries (#657)

sgouezel committed 6 years ago

46d10092

feat(algebra/order_functions): max_lt_max and min_lt_min (#692)

minchaowu committed 6 years ago

8911b8cd

feat(data/quot): quotient.ind' (#691)

kbuzzard committed 6 years ago

51f80a3f

feat(data/real): completeness criterion for Cauchy sequences (closes #654)

sgouezel committed 6 years ago

9615b385

feat(analysis/metric_space): add premetric spaces (closes #652)

sgouezel committed 6 years ago

3ac79673

feat(category/fold): `foldl` and `foldr` for `traversable` structures (#376)

cipher1024 committed 6 years ago

e93fa306

feat(analysis/normed_space): bounded linear maps with the operator norm form a normed space (closes #680)

jdsalchow committed 6 years ago

c82243a8

to_nat_le_to_nat (#685)

sgouezel committed 6 years ago

d5a1b468

fix(tactic/h_generalize): fix name resolution in h_generalize (#688)

cipher1024 committed 6 years ago

Verified 9f79d2eb

feat(tactic/replaceable): supplement `def_replacer` with attribute `replaceable`

cipher1024 committed 6 years ago

a0d8ae1e

feat(natural_isomorphism): componentwise isos are isos (#671)

kim-em committed 6 years ago

178c09d7

feat(algebra/group_power): gpow_add_one (#683)

ChrisHughes24 committed 6 years ago

Verified 9a8f1b06

remove simp on set_coe_eq_subtype (#682)

sgouezel committed 6 years ago

53952326

fix(data/*/Ico): succ_top is too aggressive as a simp lemma (#678)

kim-em committed 6 years ago

5e5f1e25

feat(data/nat/cast): abs_cast

ChrisHughes24 committed 6 years ago

25392518

feat(category_theory/kleisli): monoids, const applicative functor and kleisli categories (#660)

cipher1024 committed 6 years ago

Verified d01e523e

cleanup(*): removing uses of bare `have` (#676)

kim-em committed 6 years ago

f5bd340c

Update README.md

cipher1024 committed 6 years ago

Verified 544f35c3

fix(README): update URL for build status icon (#681)

ChrisHughes24 committed 6 years ago

Verified b3e1e6f3

feat(algebra/euclidean_domain): discrete field to euclidean domain (#674)

kckennylau committed 6 years ago

044b6fae

chore(purge_olean.sh): a few small improvements (#661)

spl committed 6 years ago

3109c4b3

fix(functor_category): remove superfluous coercions (#670)

kim-em committed 6 years ago

8590ff2b

Older