leanprover-community/mathlib

Pull Requests Commits

refactor(*): rename ordered groups/monoids to ordered add_ groups/monoids (#2347)

jcommelin committed 5 years ago

e1feab4e

chore(algebra/category): remove some [reducible] after Lean 3.8 (#2389)

kim-em committed 5 years ago

c9fca154

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

leanprover-community-bot committed 5 years ago

83359d14

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

leanprover-community-bot committed 5 years ago

4fa29249

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

bryangingechen committed 5 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 5 years ago

c68f23df

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

jcommelin committed 5 years ago

00b510eb

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

kim-em committed 5 years ago

690643ab

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

Newer Older