leanprover-community/mathlib

Pull Requests Commits

Merge branch 'master' into cauchy-rect-PRd

urkud committed 5 years ago

c6abcfec

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

feat(order/conditionally_complete_lattice): nested intervals lemma (#4848)

urkud committed 5 years ago

1521da68

feat(algebra/module/ordered): add pi instance (#4847)

urkud committed 5 years ago

f5fd2186

feat(category_theory/sites): generate lemmas (#4840)

b-mehta committed 5 years ago

6fc35175

feat(ring_theory/polynomial/basic): prerequisites for galois_definition (#4829)

tb65536 committed 5 years ago

517f0b5c

feat(data/prod): comp_map (#4826)

pechersky committed 5 years ago

0f39d7ad

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

urkud committed 5 years ago

a54c3366

urkud committed 5 years ago

508ed92d

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

urkud committed 5 years ago

836db13e

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

urkud committed 5 years ago

d84a3a0d

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

urkud committed 5 years ago

a2eebac9

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

urkud committed 5 years ago

1f72f9e1

Merge branch 'with-top-lemmas' into cauchy-rect-PRd

urkud committed 5 years ago

9dc23862

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

urkud committed 5 years ago

e878c295

Merge branch 'affine-map-eval' into cauchy-rect

urkud committed 5 years ago

e92273a0

Merge commit '6d07775db' into cauchy-rect

urkud committed 5 years ago

e435039d

Merge branch 'pi-ordered-semimodule' into cauchy-rect-PRd

urkud committed 5 years ago

09ab7143

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

urkud committed 5 years ago

3b5611d3

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

urkud committed 5 years ago

b5614f5b

urkud committed 5 years ago

aa022c0d

add affine_map.eval

urkud committed 5 years ago

6d07775d

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

urkud committed 5 years ago

a3efe827

urkud committed 5 years ago

6f7f7b4d

Newer Older