leanprover-community/mathlib3

Pull Requests Commits

feat(category_theory/iso): missing lemmas (#1001)

kim-em committed 6 years ago

6c35df0d

document the change in scripts (#1024)

cipher1024 committed 6 years ago

82f151f5

feat(Top.presheaf_ℂ): presheaves of functions to topological commutative rings (#976)

kim-em committed 6 years ago

70cd00bc

chore(Github): no need to wait for Appveyor anymopre

cipher1024 committed 6 years ago

Verified b9b5bb4b

chore(scripts): migrate scripts to own repo (#1011)

cipher1024 committed 6 years ago

e42d808b

feat(category_theory): lemmas about cancellation (#1005)

kim-em committed 6 years ago

Verified 48645152

feat(topology/maps): closed embeddings (#1013)

rwbarton committed 6 years ago

1e0761e5

feat(logic/function): comp₂ -- useful for binary operations (#993)

jcommelin committed 6 years ago

de5d0387

fix(docs/*): docs reorganization [skip ci] (#1012)

PatrickMassot committed 6 years ago

a154dedc

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

Newer Older