leanprover-community/mathlib

Pull Requests Commits

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

feat(data/dlist/basic): dlist singleton and of_list simp lemmas (#5461)

pechersky committed 5 years ago

d3a5e067

feat(data/list/basic): lemmas about scanl (#5454)

pechersky committed 5 years ago

fd9268cb

chore(analysis/asymptotics): a few more lemmas (#5482)

urkud committed 5 years ago

eb5cf252

feat(ring_theory/witt_vector): the comparison between W(F_p) and Z_p (#5164)

jcommelin committed 5 years ago

435b97ac

feat(data/list/basic): prefix simplifying iff lemmas (#5452)

pechersky committed 5 years ago

d5adbde1

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

leanprover-community-bot committed 5 years ago

24f71d7b

feat(data/list/zip): length of zip_with, nth_le of zip (#5455)

pechersky committed 5 years ago

eba2a796

fix(number_theory/bernoulli): fix docstring (#5478)

kbuzzard committed 5 years ago

3fc60fc7

chore(analysis/calculus/mean_value): use `𝓝[Ici x] x` instead of `𝓝[Ioi x] x` (#5472)

urkud committed 5 years ago

0f1362e1

feat(data/complex/is_R_or_C): register some instances (#5466)

hrmacbeth committed 5 years ago

fb99440a

chore(analysis/special_functions/trigonometric): review continuity of `tan` (#5429)

urkud committed 5 years ago

7c2f1663

refactor(analysis/inner_product_space, geometry/euclidean) range of orthogonal projection (#5408)

hrmacbeth committed 5 years ago

d569d634

feat(data/finset/basic, topology/separation): add induction_on_union, separate, and separate_finset_of_t2 (#5332)

adomani committed 5 years ago

0ff90682

chore(*): split some long lines (#5470)

urkud committed 5 years ago

02ab90cc

Newer Older