leanprover-community/mathlib

Pull Requests Commits

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

dwarn committed 5 years ago

8556499f

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

gebner committed 5 years ago

597704ac

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

leanprover-community-bot committed 5 years ago

ebdeb3b6

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

kbuzzard committed 5 years ago

29080c8c

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

kim-em committed 5 years ago

61fa4896

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

urkud committed 5 years ago

3cc7a32b

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

gebner committed 5 years ago

5169595d

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

ocfnash committed 5 years ago

bf8f25ae

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

leanprover-community-bot committed 5 years ago

1a099b38

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

kbuzzard committed 5 years ago

a7142455

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

gebner committed 5 years ago

55814dc3

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

gebner committed 5 years ago

808fa8df

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

urkud committed 5 years ago

e7582631

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

bryangingechen committed 5 years ago

f723f375

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

495deb97

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

urkud committed 5 years ago

Verified 6152d450

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

robertylewis committed 5 years ago

Verified b15c213a

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

kim-em committed 5 years ago

Verified 19e1a969

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

4a1dc427

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

alexjbest committed 5 years ago

Verified 6a7db279

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

kim-em committed 5 years ago

Verified d240f382

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

kim-em committed 5 years ago

Verified 63fc23a6

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

kbuzzard committed 5 years ago

Verified bda8a050

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

kbuzzard committed 5 years ago

Verified a8797ce7

fix(algebra/euclidean_domain): remove decidable_eq assumption (#2362)

gebner committed 5 years ago

Verified 80d3ed8f

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

67b121e4

chore(data/list): move some sections to separate files (#2341)

kim-em committed 5 years ago

Verified fbc95927

Bugfix for norm num when testing divisibility of integers (#2355)

alexjbest committed 5 years ago

Verified e4e483e5

feat(analysis/analytic/basic): change origin of power series (#2327)

sgouezel committed 5 years ago

Verified c3d9cf90

chore(scripts): update nolints.txt

leanprover-community-bot committed 5 years ago

dae7154d

Newer Older