leanprover-community/mathlib

Pull Requests Commits

feat(data/fin): val simp lemmas (#1347)

ChrisHughes24 committed 7 years ago

92fa24cf

feat(tactic/reassoc_axiom): produce associativity-friendly lemmas in category theory (#1341)

cipher1024 committed 7 years ago

Verified 6fbcc04a

fix(tactic/omega): simplify with mul_one and one_mul (#1344)

skbaek committed 7 years ago

8f09b0fb

feat(tactic/obtain): make type argument optional (#1327)

robertylewis committed 7 years ago

9c1718ab

feat(data/vector2): update_nth (#1334)

ChrisHughes24 committed 7 years ago

ab7d39b0

feat(data/vector2): to_list_map (#1335)

ChrisHughes24 committed 7 years ago

538d3f6f

feat(data/list/basic): list.mem_insert_nth (#1336)

ChrisHughes24 committed 7 years ago

66fa499b

feat(linear_algebra/matrix): linear maps are linearly equivalent to matrices (#1310)

CPutz committed 7 years ago

a1dda1e9

feat(tactic/sanity_check): add #sanity_check command (#1318)

fpvandoorn committed 7 years ago

2e76f364

feat(tactic/finish): parse ematch lemmas with `finish using ...` (#1326)

jesse-michael-han committed 7 years ago

397c0169

feat(analysis/complex/exponential): prove that rpow is continuous (#1306)

Zhouhang Zhou committed 7 years ago

2e90bed8

feat(*): lemmas needed for two projects (#1294)

fpvandoorn committed 7 years ago

74c25a57

feat(data/rat): move lemmas to right file, add nat cast lemmas, remove (#1333)

kappelmann committed 7 years ago

fa68342d

refactor(data/fintype): shorten proof of card_eq (#1332)

ChrisHughes24 committed 7 years ago

73cc56c5

doc(contribute/style): remove outdated syntax [ci skip] (#1329)

robertylewis committed 7 years ago

ebbbb76b

chore(category_theory/isomorphism): docstring, DRY, add some trivial lemmas (#1309)

urkud committed 7 years ago

3d512f79

chore(*): migrate `units.map` to bundled homs (#1331)

urkud committed 7 years ago

e48ad0dc

fix(data/mllist): fix off-by-one bug in mllist.take (#1298)

Lucas Allen committed 7 years ago

02548ad6

feat(data/pequiv): symm_single_apply (#1324)

ChrisHughes24 committed 7 years ago

0bc4a400

fix(.github): typo (#1323)

fpvandoorn committed 7 years ago

2a131d9f

fix(algebra/ring): fix typo in docstring (#1322)

kbuzzard committed 7 years ago

5796465f

feat(scripts): add scripts to import all mathlib files (#1281)

fpvandoorn committed 7 years ago

900c53ae

doc(contribute): add link to doc requirements (#1317)

robertylewis committed 7 years ago

Verified df1fb07d

feat(data/fin): mem_find_iff (#1307)

ChrisHughes24 committed 7 years ago

92a54240

feat(algebra/ordered_field): le_div_iff_of_neg (#1311)

ChrisHughes24 committed 7 years ago

f46b0dc6

feat(data/option/basic): bind_eq_none' (#1312)

ChrisHughes24 committed 7 years ago

3bd3dcd5

feat(algebra/ordered_ring): pos_of_mul_neg_left and similar (#1313)

ChrisHughes24 committed 7 years ago

01cb33cb

Delete repeated item (#1316)

Zhouhang Zhou committed 7 years ago

37d4edab

feat(data/matrix/pequiv): partial equivalences to represent matrices (#1228)

ChrisHughes24 committed 7 years ago

3aad7f1e

feat(archive): add archive (#1295)

fpvandoorn committed 7 years ago

a79794ab

Newer Older