leanprover-community/mathlib

Pull Requests Commits

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

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

chore(data/finset/basic): a few lemmas about `finset.piecewise` (#4852)

urkud committed 5 years ago

f9c8abe3

chore(linear_algebra/affine_space/ordered): compare endpoints to midpoint (#4851)

urkud committed 5 years ago

7756265e

feat(linear_algebra/affine_space/affine_map): add `affine_map.proj` (#4850)

urkud committed 5 years ago

1f616214

refactor(data/pnat): move data.pnat.prime (#4839)

digama0 committed 5 years ago

6a449305

feat(data/dfinsupp): Port `finsupp.lsum` and lemmas about `lift_add_hom` (#4833)

eric-wieser committed 5 years ago

3b2c97f9

feat(data/dfinsupp): Add dfinsupp.single_eq_single_iff, and subtype.heq_iff_coe_eq (#4810)

eric-wieser committed 5 years ago

17697a60

feat(analysis/normed_space/add_torsor): distance to midpoint (#4849)

urkud committed 5 years ago

67c2b5a0

Newer Older