leanprover-community/mathlib

Pull Requests Commits

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

leanprover-community-bot committed 5 years ago

a206df1e

refactor(normed_space): require `norm_smul_le` instead of `norm_smul` (#2693)

urkud committed 5 years ago

b530cdb4

chore(algebra/ring): drop an unneeded instance (#2705)

urkud committed 5 years ago

39af0f66

fix(algebra/big_operators): typo fix (#2704)

jsm28 committed 5 years ago

1580cd87

feat(archive/100-theorems-list): Sum of the Reciprocals of the Triangular Numbers (#2692)

jalex-stark committed 5 years ago

4f484a1e

feat(ring_theory/ideal_operations): jacobson radical, is_local, and primary ideals (#768)

kckennylau committed 5 years ago

21bdb787

refactor(group_theory/monoid_localization): use old_structure_cmd (#2683)

101damnations committed 5 years ago

00024db7

feat(data/finset): remove uses of choice for infima (#2699)

b-mehta committed 5 years ago

a7b17cdd

feat(data/finset) Another finset disjointness lemma (#2698)

Smaug123 committed 5 years ago

c81be77b

doc(tactic/solve_by_elim): improve docs (#2696)

kim-em committed 5 years ago

4b71428d

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

Newer Older