leanprover-community/mathlib3

Pull Requests Commits

docs(elan): remove reference to nightly Lean (#928)

jcommelin committed 6 years ago

f01934c6

fix(algebra.field): introduce division_ring_has_div' (#852)

abhimanyupallavisudhir committed 6 years ago

49c3a049

feat(algebra/free): free magma, semigroup, monoid (#735)

kckennylau committed 6 years ago

3fe449e1

refactor(data/int/basic): weaken hypotheses for int.induction_on (#887)

ChrisHughes24 committed 6 years ago

be79f25b

feat(submonoid, subgroup, subring): is_ring_hom instances for set.inclusion (#917)

ChrisHughes24 committed 6 years ago

36f0c224

fix(tactic/explode): more accurate may_be_proof (#924)

digama0 committed 6 years ago

Verified c1e07a2e

minor changes (#921)

kim-em committed 6 years ago

22fcb4e9

feat(analysis/normed_space/deriv): show that the differential is unique (2) (#916)

jdsalchow committed 6 years ago

f5d43a95

rename has_sum and is_sum to summable and has_sum (#912)

sgouezel committed 6 years ago

41014e50

fix(mergify): merge if either push or pr build passes. (#918)

ChrisHughes24 committed 6 years ago

Verified c4b65da1

refactor(order/lexicographic): use prod.lex and psigma.lex (#914)

minchaowu committed 6 years ago

49ccc9f7

fix(category_theory): make the `nat_trans` arrow `⟹` a synonym for the `hom` arrow (#907)

kim-em committed 6 years ago

89924726

feat(category_theory): iso_whisker_(left|right) (#908)

kim-em committed 6 years ago

f04535de

refactor(algebra/group): is_monoid_hom extends is_mul_hom (#915)

jcommelin committed 6 years ago

86bd577c

feat(data/set/basic): inclusion map (#906)

ChrisHughes24 committed 6 years ago

f1683a9e

refactor(category_theory): rename `functor.on_iso` to `functor.map_iso` (#893)

kim-em committed 6 years ago

96d748eb

reorganising category_theory/instances/rings.lean (#909)

kim-em committed 6 years ago

d692499e

feat(field_theory/subfield): subfields are fields (#888)

ChrisHughes24 committed 6 years ago

4494001d

chore(build): allow PRs from separate repos to test deployment scripts

cipher1024 committed 6 years ago

5c4f5f20

fix(mergify): require travis "push" check to push (#913)

ChrisHughes24 committed 6 years ago

c2d79f85

refactor(*): rename is_group_hom.mul to map_mul (#911)

jcommelin committed 6 years ago

66a86ffe

feat(order/lexicographic): lexicographic pre/partial/linear orders (#820)

kim-em committed 6 years ago

eb024dc8

feat(group_theory/subgroup): subtype.add_comm_group (#903)

ChrisHughes24 committed 6 years ago

Verified 29507a4b

feat(category_theory/colimits): missing simp lemmas (#894)

kim-em committed 6 years ago

ec51b6e1

fix(doc/extra/tactic_writing): rename mul_left (#902) [ci skip]

minchaowu committed 6 years ago

6d2cf4ae

feat(linear_algebra/dual): add dual vector spaces (#881)

faabian committed 6 years ago

5f1329a2

feat(analysis/complex/polynomial): fundamental theorem of algebra (#851)

ChrisHughes24 committed 6 years ago

10490ea7

feat(topology/gromov_hausdorff): the Gromov-Hausdorff space (#883)

sgouezel committed 6 years ago

4fecb101

trying to work out what was wrong with catching signals (#898)

kim-em committed 6 years ago

5d81ab17

fix(category_theory): turn `has_limits` classes into structures (#896)

kim-em committed 6 years ago

0a490302

Newer Older