leanprover-community/mathlib

Pull Requests Commits

feat(order/filter/at_top_bot): lemmas about `map/comap` of `at_top`/`at_bot` (#4878)

urkud committed 5 years ago

d88042c1

feat(data/quaternion): define quaternions and prove some basic properties (#2339)

urkud committed 5 years ago

7ab3ca85

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

leanprover-community-bot committed 5 years ago

16e38718

feat(category_theory/yoneda): type level yoneda equivalence (#4889)

b-mehta committed 5 years ago

23a2767d

feat(order): countable categoricity of dense linear orders (#2860)

dwarn committed 5 years ago

505097f4

chore(algebra/lie): adjoint rep of lie algebra uses lowercase `ad` (#4891)

jcommelin committed 5 years ago

712a0b75

feat(*): assorted prereqs for cyclotomic polynomials (#4887)

riccardobrasca committed 5 years ago

e88a5bb5

feat(category_theory/limits/types): ext iff lemma (#4883)

b-mehta committed 5 years ago

b37d4a3d

fix(tactic/interactive): issue where long term tooltips break layout (#4882)

EdAyers committed 5 years ago

6bed7d4f

feat(tactic/mk_iff_of_inductive_prop): mk_iff attribute (#4863)

bryangingechen committed 5 years ago

4f8c490f

feat(category_theory/limits/types): explicit description of equalizers in Type (#4880)

b-mehta committed 5 years ago

918e28ca

chore(data/set/intervals/ord_connected): make it more useful as a typeclass (#4879)

urkud committed 5 years ago

34c3668e

feat(*/multilinear): define `(continuous_)multilinear_map.restrict_scalars` (#4872)

urkud committed 5 years ago

9851a886

chore(category_theory/limits): Use `lim_map` over `lim.map` (#4856)

b-mehta committed 5 years ago

63d109fe

feat(category_theory/limits/shapes/products): pi comparison morphism (#4855)

b-mehta committed 5 years ago

b26fc59f

feat(algebra/operations): add three lemmas (#4864)

faenuccio committed 5 years ago

52756281

feat(linear_algebra/matrix): `det (reindex e e A) = det A` (#4875)

Vierkantor committed 5 years ago

c2b6220c

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

leanprover-community-bot committed 5 years ago

57ee2162

chore(scripts): typo in yaml_check (#4881)

hrmacbeth committed 5 years ago

0e4f8f41

chore(data/finsupp/basic): Remove finsupp.leval which duplicates finsupp.lapply (#4876)

eric-wieser committed 5 years ago

dae87bcd

chore(data/fintype/card): add a few lemmas (#4877)

urkud committed 5 years ago

5334f48b

chore({data,linear_algebra}/dfinsupp): Move linear_algebra stuff to its own file (#4873)

eric-wieser committed 5 years ago

13a104d9

feat(algebra/algebra/subalgebra): subalgebras, when seen as submodules, are idempotent (#4854)

laughinggas committed 5 years ago

6587e840

chore(order/basic): move `strict_mono_coe`to `subtype` NS (#4870)

urkud committed 5 years ago

0aa6aed9

refactor(data/list/basic,...): more explicit args (#4866)

digama0 committed 5 years ago

309df10a

feat(ring_theory/polynomial/content): monic polynomials are primitive (#4862)

awainverse committed 5 years ago

556079b4

fix(tactic/simpa): reflect more simp errors (#4865)

digama0 committed 5 years ago

ecdc3197

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

leanprover-community-bot committed 5 years ago

7c8868d8

doc(*): work around markdown2 bug for now (#4842)

robertylewis committed 5 years ago

4aa087aa

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

leanprover-community-bot committed 5 years ago

7a624b88

Newer Older