leanprover-community/mathlib

Pull Requests Commits

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

Merge branch 'master' into cauchy-rect

urkud committed 5 years ago

6b287306

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

urkud committed 5 years ago

6098ec05

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

leanprover-community-bot committed 5 years ago

7a624b88

docs(order/complete_lattice): make two docstrings more detailed (#4859)

hrmacbeth committed 5 years ago

6f7c5394

refactor(tactic/norm_num): move norm_num extensions (#4822)

digama0 committed 5 years ago

51cbb836

feat(category_theory/sites): functor inclusion constructions (#4845)

b-mehta committed 5 years ago

be161d11

chore(group_theory/group_action): introduce `smul_comm_class` (#4770)

urkud committed 5 years ago

d91c8785

chore(algebra/ordered_group): use implicit args, add `add_eq_coe` (#4853)

urkud committed 5 years ago

9a03bdf1

refactor(order/filter): move some proofs to `bases` (#3478)

urkud committed 5 years ago

e14c3782

urkud committed 5 years ago

dbd5e562

Merge branch 'cauchy-rect-PRd' into cauchy-rect

urkud committed 5 years ago

8e80db99

Newer Older