leanprover-community/mathlib

Pull Requests Commits

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

leanprover-community-bot committed 5 years ago

611b73eb

feat(field_theory/algebraic_closure): algebraically closed fields have no nontrivial algebraic extensions (#5537)

dtumad committed 5 years ago

9c46cadc

chore(algebra/field): use `K` as a type variable (#5535)

urkud committed 5 years ago

6e0d0fa4

feat(measure_theory): various additions (#5389)

fpvandoorn committed 5 years ago

99881936

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

awainverse committed 5 years ago

f1d2bc60

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

Newer Older