leanprover-community/mathlib3

Pull Requests Commits

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

leanprover-community-bot committed 6 years ago

83359d14

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

leanprover-community-bot committed 6 years ago

4fa29249

feat(actions): manage labels on PR review (#2387)

bryangingechen committed 6 years ago

81d8104f

chore(category_theory/types): add documentation, remove bad simp lemmas and instances, add notation for functions as morphisms (#2383)

kim-em committed 6 years ago

c68f23df

perf(data/*): add inline attributes (#2380)

jcommelin committed 6 years ago

00b510eb

fix(tactic/equiv_rw): don't use `subst` unnecessarily (#2334)

kim-em committed 6 years ago

690643ab

feat(category_theory): make defining groupoids easier (#2360)

dwarn committed 6 years ago

8556499f

chore(*): switch to lean 3.8.0 (#2361)

gebner committed 6 years ago

597704ac

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

leanprover-community-bot committed 6 years ago

ebdeb3b6

feat(data/list/range): add sum lemmas (#2385)

kbuzzard committed 6 years ago

29080c8c

feat(tactic/trunc_cases): a tactic for case analysis on trunc hypotheses (#2368)

kim-em committed 6 years ago

61fa4896

feat(order/complete_lattice): add a constructor from `partial_order` and `Inf` (#2359)

urkud committed 6 years ago

3cc7a32b

chore(tactic/omega): add trace.omega option to show internal representation (#2377)

gebner committed 6 years ago

5169595d

feat(algebra/lie_algebra): quotients of Lie modules are Lie modules (#2335)

ocfnash committed 6 years ago

bf8f25ae

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

leanprover-community-bot committed 6 years ago

1a099b38

feat(group_theory/order_of_element): order_of_dvd_iff_pow_eq_one (#2364)

kbuzzard committed 6 years ago

a7142455

fix(.github/workflows/add_label): add missing outputs (#2379)

gebner committed 6 years ago

55814dc3

chore(.github): remove linebreaks from pull request template (#2378)

gebner committed 6 years ago

808fa8df

refactor(ring_theory/algebra): use bundled homs, allow semirings (#2303)

urkud committed 6 years ago

e7582631

feat(ci): switch from mergify to bors (#2322)

bryangingechen committed 6 years ago

f723f375

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

495deb97

refactor(field_theory/perfect_closure): use bundled homs, review (#2357)

urkud committed 6 years ago

Verified 6152d450

chore(*): replace uses of `---` delimiter in tactic docs (#2372)

robertylewis committed 6 years ago

Verified b15c213a

doc(add_tactic_doc): slight improvement to docs (#2365)

kim-em committed 6 years ago

Verified 19e1a969

chore(scripts): update nolints.txt

leanprover-community-bot committed 6 years ago

4a1dc427

feat(tactic/ring_exp) allow ring_exp inside of conv blocks (#2369)

alexjbest committed 6 years ago

Verified 6a7db279

feat(tactic/simp_result): tactics for simplifying the results of other tactics (#2356)

kim-em committed 6 years ago

Verified d240f382

feat(data/list): chain_iff_nth_le (#2354)

kim-em committed 6 years ago

Verified 63fc23a6

doc(docs/extras/tactic_writing) add cheap method (#2198)

kbuzzard committed 6 years ago

Verified bda8a050

feat(data/set/basic): add lemmata (#2353)

kbuzzard committed 6 years ago

Verified a8797ce7

Newer Older