leanprover-community/mathlib3

Pull Requests Commits

chore(build): remove script testing on PRs [skip ci]

cipher1024 committed 6 years ago

Verified 8e71ceec

docs(algebra/ring): document compatibility hack [skip ci]

cipher1024 committed 6 years ago

Verified e6d959df

chore(compatibility): compatibility with Lean 3.5.0c (#1007)

cipher1024 committed 6 years ago

Verified c7d870e8

feat(data/polynomial): degree_eq_one_of_irreducible_of_root (#1010)

ChrisHughes24 committed 6 years ago

60da4f4d

refactor(algebra/associated): rename nonzero_of_irreducible to ne_zero_of_irreducible (#1009)

ChrisHughes24 committed 6 years ago

8603e6b0

fix(category/fold): use correct `opposite` (#1008)

rwbarton committed 6 years ago

6858c2f7

fix(tactic/basic): missing `conv` from tactic.basic (#1004)

kim-em committed 6 years ago

91a7fc23

feat(set_theory): add to cardinal, ordinal, cofinality (#963)

fpvandoorn committed 6 years ago

e66e1f30

feat(algebra/pointwise): More lemmas on pointwise multiplication (#997)

jcommelin committed 6 years ago

5329bf3a

refactor(strict_mono): make definition + move to order_functions (#998)

jcommelin committed 6 years ago

df5eddeb

refactor(order/basic): make type class args explicit in {*}order.lift (#995)

jcommelin committed 6 years ago

8f5d2401

feat(*): preorder instances for with_bot and with_zero (#996)

jcommelin committed 6 years ago

7f9717fd

chore(tactics): splitting tactics and tests into more files (#985)

kim-em committed 6 years ago

c9cfafc9

feat(group_theory/subgroup): is_subgroup.inter (#994)

jcommelin committed 6 years ago

73a30da3

feat(category_theory/category_of_elements) (#990)

kim-em committed 6 years ago

Verified 87cf6e36

building the hyperreal library (#835)

abhimanyupallavisudhir committed 6 years ago

820bac36

feat(scripts): add --build-new flag to cache-olean (#992)

kim-em committed 6 years ago

4a38d2e1

chore(build): cron build restarts from scratch

cipher1024 committed 6 years ago

717033e3

feat(category/monad/cont): monad_cont instances for state_t, reader_t, except_t and option_t (#733)

cipher1024 committed 6 years ago

c726c128

chore(build): fix stages in cron job

cipher1024 committed 6 years ago

98ba07bc

chore(build): build against Lean 3.5 nightly build (#989)

cipher1024 committed 6 years ago

Verified 505f748b

feat(category_theory): currying for functors (#981)

kim-em committed 6 years ago

6eba20b0

six(style.md): fix broken code (#987)

fpvandoorn committed 6 years ago

f536dac8

feat(ring_theory/adjoin): adjoining elements to form subalgebras (#756)

kckennylau committed 6 years ago

23270e71

feat(category_theory/products): associators (#982)

kim-em committed 6 years ago

3f26ba88

feat(presheaves) (#886)

kim-em committed 6 years ago

1e8f438c

feat(data/set/basic): prod_subset_iff (#980)

kim-em committed 6 years ago

fc8b08b3

fix(data/set/finite): make fintype_seq an instance (#979)

kim-em committed 6 years ago

fbce6e4d

feat(logic/basic): forall_iff_forall_surj (#977)

kim-em committed 6 years ago

7dea60ba

feat(colimits): arbitrary colimits in Mon and CommRing (#910)

kim-em committed 6 years ago

b4d483e2

Newer Older