leanprover-community/mathlib

Pull Requests Commits

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

feat(ring_theory/power_series): define power series for `exp`, `sin`, `cos`, and `1 / (u - x)`. (#5432)

urkud committed 5 years ago

4ddae3db

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

leanprover-community-bot committed 5 years ago

92dfdbcc

fix(group_theory/*, algebra/group): [to_additive, simp] doesn't work (#5468)

kbuzzard committed 5 years ago

3c7394fe

chore(data/{equiv,set}/basic): image_preimage (#5465)

urkud committed 5 years ago

9ec2778f

feat(data/list/basic): lemmas about nth of take and append (#5449)

pechersky committed 5 years ago

d2ae43f6

feat(data/ordmap): Ordered maps (like rb_map but better) (#5353)

digama0 committed 5 years ago

3b9cbdfe

feat(linear_algebra/tensor_algebra): Add missing lemmas about subtraction (#5428)

eric-wieser committed 5 years ago

bc3ad25a

feat(data/option/basic): lemmas on map of none and congr (#5424)

pechersky committed 5 years ago

34d5750f

feat(ring_theory/perfection): define characteristic predicate of perfection (#5386)

kckennylau committed 5 years ago

0ed425fa

feat(ring_theory/roots_of_unity): add minimal_polynomial_eq_pow (#5444)

riccardobrasca committed 5 years ago

96a2aa1d

feat(category_theory/yoneda): add iso_comp_punit (#5448)

kbuzzard committed 5 years ago

c5c02ec8

feat(category_theory/limits): yoneda preserves limits (#5439)

b-mehta committed 5 years ago

c98d5bb0

chore(category_theory/sites/sheaf): rename sheaf to sheaf_of_types (#5458)

kbuzzard committed 5 years ago

4778e165

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

leanprover-community-bot committed 5 years ago

ca2e536f

feat(tactic/field_simp): let field_simp use norm_num to prove numerals are nonzero (#5418)

sgouezel committed 5 years ago

d79105ef

feat(topology/algebra/ordered): continuity of `abs` (#5412)

urkud committed 5 years ago

50107383

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

leanprover-community-bot committed 5 years ago

a9fb069b

feat(field_theory/galois): Separable splitting field is Galois (#5347)

tb65536 committed 5 years ago

1cb97275

Older