leanprover-community/mathlib

Pull Requests Commits

hrmacbeth committed 4 years ago

e7c364ea

hrmacbeth committed 4 years ago

0f4c6656

hrmacbeth committed 4 years ago

b5d67216

might as well do `deriv_fpow` too (WIP)

hrmacbeth committed 4 years ago

cad49054

Merge branch 'master' into continuous_at_inv_iff

hrmacbeth committed 4 years ago

7eab27f6

feat(order/lattice_intervals): lattice structures on intervals in lattices (#5496)

awainverse committed 4 years ago

f1d2bc60

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

urkud committed 4 years ago

16320e2e

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

urkud committed 4 years ago

958c407a

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

urkud committed 4 years ago

b15bb06e

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

urkud committed 4 years ago

38ba6ba2

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

hrmacbeth committed 4 years ago

c82be35d

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

urkud committed 4 years ago

7a031718

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

urkud committed 4 years ago

8545aa60

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

jcommelin committed 4 years ago

5e86589d

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

robertylewis committed 4 years ago

1c110ada

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

leanprover-community-bot committed 4 years ago

7c6020f1

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

dupuisf committed 4 years ago

abffbaa3

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

awainverse committed 4 years ago

8e413ebb

doc(localized): update documentation (#5519)

fpvandoorn committed 4 years ago

15ff8653

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

leanprover-community-bot committed 4 years ago

297d97ea

let simp compute deriv inv

hrmacbeth committed 4 years ago

2b1d665c

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

tb65536 committed 4 years ago

41bad637

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

tb65536 committed 4 years ago

d245c4e0

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

b-mehta committed 4 years ago

f1f2ca68

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

leanprover-community-bot committed 4 years ago

6d1d4c13

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

digama0 committed 4 years ago

6d0b415e

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

awainverse committed 4 years ago

5c8c1222

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

pechersky committed 4 years ago

1e75453f

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

pechersky committed 4 years ago

f7e728ad

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

urkud committed 4 years ago

ae60bb96

Older