leanprover-community/mathlib

Pull Requests Commits

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

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

leanprover-community-bot committed 5 years ago

1f0231df

feat(algebra/*): Noncomputable `group` structures from `is_unit` (#5427)

awainverse committed 5 years ago

feced767

feat(data/list/basic): lemmas about reduce_option (#5450)

pechersky committed 5 years ago

f300c759

chore(linear_algebra/linear_independent): make a binding explicit in ne_zero (#5494)

Julian committed 5 years ago

3046436c

chore(ring_theory/power_series/well_known): generalize (#5491)

urkud committed 5 years ago

46614b02

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

leanprover-community-bot committed 5 years ago

8a038398

feat(field_theory/galois): is_galois.self (#5486)

tb65536 committed 5 years ago

2ae61be9

feat(data/list/chain): relate chain to refl trans gen (#5437)

b-mehta committed 5 years ago

63070edc

chore(group_theory/coset): Make `quotient_group.mk` an abbreviation (#5377)

eric-wieser committed 5 years ago

ceae5296

feat(group_theory/*): mark some lemmas as ext (about homs out of free constructions) (#5484)

jcommelin committed 5 years ago

2a5a0b0e

chore(order/filter/basic): make `filter.univ_mem_sets` a `simp` lemma (#5464)

urkud committed 5 years ago

e2edba53

Newer Older