leanprover-community/mathlib

Pull Requests Commits

feat(category_theory/limits/shapes): avoid choice for binary products (#2695)

b-mehta committed 5 years ago

74286f51

chore(*): bump to lean-3.12.0 (#2681)

jcommelin committed 5 years ago

1b85e3c2

feat(analysis/special_functions/exp_log): power series for log around 1 (#2646)

sgouezel committed 5 years ago

f5f7a3cf

fix(tactic/norm_num): div/mod with negative first arg (#2689)

digama0 committed 5 years ago

14a82b30

chore(scripts): update nolints.txt (#2690)

leanprover-community-bot committed 5 years ago

a4266a01

perf(tactic/ring): use new norm_num, avoid mk_app (#2685)

digama0 committed 5 years ago

471d29e8

chore(data/int/basic): mark cast_sub with simp attribute (#2687)

ChrisHughes24 committed 5 years ago

b44fa3ca

feat(category_theory/limits/lattice): finite limits in a semilattice (#2665)

b-mehta committed 5 years ago

f07ac364

feat(data/nat/choose): Sum a row of Pascal's triangle (#2684)

Smaug123 committed 5 years ago

378aa0d7

chore(scripts): update nolints.txt (#2682)

leanprover-community-bot committed 5 years ago

be03a3d4

perf(tactic/ext): NEVER USE `user_attribute.get_param` (#2674)

gebner committed 5 years ago

606be81d

feat(topology): a few properties of `tendsto _ _ (𝓤 α)` (#2645)

urkud committed 5 years ago

7427f8e0

chore(algebra/ring): lemmas about units in a semiring (#2680)

101damnations committed 5 years ago

d412cfd0

chore(scripts): update nolints.txt (#2679)

leanprover-community-bot committed 5 years ago

03c272e5

chore(logic/function): drop `function.uncurry'` (#2678)

urkud committed 5 years ago

2871bd1e

chore(linear_algebra/basis): use dot notation, simplify some proofs (#2671)

urkud committed 5 years ago

3da777aa

doc(*): move most docs to website, update links (#2676)

bryangingechen committed 5 years ago

d0beb496

chore(logic/function): move to `logic/function/basic` (#2677)

urkud committed 5 years ago

7077b588

chore(algebra/free_monoid): add a custom `rec_on` (#2670)

urkud committed 5 years ago

6ffb6137

refactor(order/lattice): adjust proofs to avoid choice (#2666)

b-mehta committed 5 years ago

f7cb3634

refactor(scripts/mk_all): generate a single deterministic all.lean file (#2673)

gebner committed 5 years ago

fc0c0258

feat(topology/algebra/infinite_sum): sums on subtypes (#2659)

sgouezel committed 5 years ago

9f16f866

chore(scripts): update nolints.txt (#2669)

leanprover-community-bot committed 5 years ago

c9f2cbcd

feat(category_theory): preadditive categories (#2663)

TwoFX committed 5 years ago

506a71f9

feat(analysis/calculus/(f)deriv): differentiability of a finite sum of functions (#2657)

sgouezel committed 5 years ago

ce86d33b

chore(group_theory/submonoid): use `complete_lattice_of_Inf` (#2661)

urkud committed 5 years ago

ed183f95

feat(topology/separation): add `subtype.t1_space` and `subtype.regular` (#2667)

urkud committed 5 years ago

51e2b4cc

feat(topology/bounded_continuous_function): the normed space C^0 (#2660)

hrmacbeth committed 5 years ago

4857284a

feat(analysis/specific_limits): more geometric series (#2658)

sgouezel committed 5 years ago

cbffb34c

feat(category_theory/creates): creates limits => preserves limits (#2639)

b-mehta committed 5 years ago

437fdaf8

Newer Older