leanprover-community/mathlib

Pull Requests Commits

chore(data/finset): rename le_min_of_mem to min_le_of_mem (#1231)

ChrisHughes24 committed 6 years ago

92ac50cb

feat(data/option/basic): bind_eq_none (#1232)

ChrisHughes24 committed 6 years ago

7217f134

chore(data/fintype): change `unique.fintype` to priority 0 (#1230)

ChrisHughes24 committed 6 years ago

46074fc1

feat(tactic/rcases): add obtain tactic (#1218)

robertylewis committed 6 years ago

0e9ac849

feat(data/pequiv): partial equivalences (#1206)

ChrisHughes24 committed 6 years ago

dcf01308

chore(algebra/group/hom): add `is_monoid_hom.of_mul`, use it (#1225)

urkud committed 6 years ago

03e6d0ea

feat(pformat): provide `trace!` and `fail!` and allow tactic values (#1222)

cipher1024 committed 6 years ago

51f26459

feat(logic,data/equiv,prod): various lemmas (#1224)

cipher1024 committed 6 years ago

a1cfc5cc

feat(data/{nat,int}/parity): the 'even' predicate on nat and int (#1219)

avigad committed 6 years ago

0eea0d9f

feat(data/finmap): extend the API (#1223)

cipher1024 committed 6 years ago

6db58292

chore(data/src/pending): remove unused folder (#1221)

avigad committed 6 years ago

5a48be3e

feat(data/{nat,int,zmod,finset}): add a few useful facts (#1220)

avigad committed 6 years ago

fb7dfa16

feat(analysis/calculus/mean_value): the mean value inequality (#1212)

sgouezel committed 6 years ago

3d36966e

feat(analysis/calculus/deriv): extended API for derivatives (#1213)

sgouezel committed 6 years ago

78065861

feat(tactic/localized): localized notation (#1081)

fpvandoorn committed 6 years ago

2511faf4

refactor(*): change priority of \simeq (#1210)

fpvandoorn committed 6 years ago

c2cc9a99

refactor(*): make `is_group_hom` extend `is_mul_hom` (#1214)

urkud committed 6 years ago

86d0f292

perf(algebraic_geometry/presheafed_space): replace/optimize tidy scripts (#1204)

robertylewis committed 6 years ago

1b1c64b0

feat(algebra/ordered_ring): with_top.nat_induction (#1211)

sgouezel committed 6 years ago

cc5870db

feat(*): Miscellaneous lemmas in algebra (#1188)

jcommelin committed 6 years ago

5cdebb75

fix(*): fix line endings (#1209)

fpvandoorn committed 6 years ago

5aebdc43

feat(tactic/apply_fun): adds `apply_fun` tactic (#1184)

PatrickMassot committed 6 years ago

0bc4a50d

feat(data/list/basic): list.prod_range_succ, list.sum_range_succ (#1197)

bryangingechen committed 6 years ago

d2b4380c

docs(contribute/index.md): #1131 [skip ci]

cipher1024 committed 6 years ago

Verified 8939d951

doc(README): Add link to website

digama0 committed 6 years ago

Verified b00460c0

refactor(topology/algebra/open_subgroup) Finish TODO (#1202)

Zhouhang Zhou committed 6 years ago

fb1848bb

feat(analysis/calculus/tangent_cone): more properties of the tangent cone (#1136)

sgouezel committed 6 years ago

e25a5970

feat(meta/pformat): format! macro using `pp` instead of `to_fmt` (#1194)

cipher1024 committed 6 years ago

0cd0d4ed

refactor(category_theory/endomorphism): move to a dedicated file; prove simple lemmas (#1195)

urkud committed 6 years ago

60e4bb92

refactor(topology/*): define and use dense_inducing (#1193)

PatrickMassot committed 6 years ago

3a7c661a

Newer Older