leanprover-community/mathlib3

Pull Requests Commits

chore(topology/algebra/infinite_sum): refactor `tsum_mul_left/right` (#5533)

urkud committed 5 years ago

16320e2e

chore(analysis/normed_space/basic): a few lemmas about `nnnorm` (#5532)

urkud committed 5 years ago

958c407a

feat(topology/instances/ennreal): a sufficient condition for `f : (Σ i, β i) → ℝ` to be summable (#5531)

urkud committed 5 years ago

b15bb06e

chore(data/real/{e,}nnreal): a few lemmas (#5530)

urkud committed 5 years ago

38ba6ba2

feat(analysis/normed_space/inner_product): orthogonal complement lemmas (#5474)

hrmacbeth committed 5 years ago

c82be35d

chore(order/rel_iso): add some missing lemmas (#5492)

urkud committed 5 years ago

7a031718

chore(topology/algebra/ordered): move code, add missing lemmas (#5481)

urkud committed 5 years ago

8545aa60

chore(data/nat/enat): some useful lemmas (#5517)

jcommelin committed 5 years ago

5e86589d

fix(tactic/linarith): elaborate and insert arguments before destructing hypotheses (#5501)

robertylewis committed 5 years ago

1c110ada

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

leanprover-community-bot committed 5 years ago

7c6020f1

feat(analysis/convex/specific_functions): log is concave (#5508)

dupuisf committed 5 years ago

abffbaa3

feat(order/bounded_lattice): define atoms, coatoms, and simple lattices (#5471)

awainverse committed 5 years ago

8e413ebb

doc(localized): update documentation (#5519)

fpvandoorn committed 5 years ago

15ff8653

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

leanprover-community-bot committed 5 years ago

297d97ea

feat(polynomial/degree/definitions): nat_degree_X_pow (#5512)

tb65536 committed 5 years ago

41bad637

feat(polynomial/algebra_map): aeval_comp (#5511)

tb65536 committed 5 years ago

d245c4e0

feat(category_theory/limits): preserves limits of equivalent shape (#5515)

b-mehta committed 5 years ago

f1f2ca68

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

leanprover-community-bot committed 5 years ago

6d1d4c13

feat(data/list/basic): nth_zero (#5513)

digama0 committed 5 years ago

6d0b415e

chore(analysis/analytic/basic): speed up slow lemmas (#5507)

awainverse committed 5 years ago

5c8c1222

feat(data/list/basic): filter_map retains prefix (#5453)

pechersky committed 5 years ago

1e75453f

feat(data/list/range): enum is a zip (#5457)

pechersky committed 5 years ago

f7e728ad

chore(topology/algebra/order): add `continuous_on.surj_on_of_tendsto` (#5502)

urkud committed 5 years ago

ae60bb96

feat(ring_theory/perfection): perfection.map (#5503)

kckennylau committed 5 years ago

add100aa

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

leanprover-community-bot committed 5 years ago

768497cd

fix(algebra/big_operators/basic): add docstrings for `sum_bij` and `sum_bij'` (#5497)

kbuzzard committed 5 years ago

666035fa

chore(topology/homeomorph): a few more lemmas, golf (#5467)

urkud committed 5 years ago

1a526b31

feat(analysis/specific_limits): a `tfae` about "`f` grows exponentially slower than `R ^ n`" (#5488)

urkud committed 5 years ago

726b7bfd

feat(category_theory/limits): yoneda reflects limits (#5447)

b-mehta committed 5 years ago

d968a61d

chore(logic/basic): +2 simp lemmas (#5500)

urkud committed 5 years ago

f60fd080

Newer Older