leanprover-community/mathlib

Pull Requests Commits

Do we have the comparison test for series convergence?

stuart-presnell committed 3 years ago

e148db04

Outline proof;Add material from Vladimir Goryachev & Stepan Nesterov

stuart-presnell committed 3 years ago

f4b49f3e

Fix Authors line

stuart-presnell committed 3 years ago

18ad9b97

stuart-presnell committed 3 years ago

858d07eb

Create prime_reciprocals.lean

stuart-presnell committed 4 years ago

37596f04

feat(data/nat/prime): factors sublist of product (#11104)

b-mehta committed 4 years ago

4daaff06

refactor(order/lexicographic): Change the `lex` synonym (#10926)

YaelDillies committed 4 years ago

62d814a4

feat(measure_theory/function/lp_space): use has_measurable_add2 instead of second_countable_topology (#11202)

RemyDegenne committed 4 years ago

9d0fd523

feat(analysis/inner_product_space/basic): negating orthonormal vectors (#11208)

jsm28 committed 4 years ago

72498958

feat(*/cyclotomic): update is_root_cyclotomic_iff to use ne_zero (#11071)

ericrbg committed 4 years ago

83f40364

feat(linear_algebra/matrix/basis): `to_matrix_units_smul` and `to_matrix_is_unit_smul` (#11191)

jsm28 committed 4 years ago

236d978d

feat(combinatorics/configuration): `has_lines` implies `has_points`, and vice versa (#11170)

tb65536 committed 4 years ago

4b3198b9

feat(algebra/big_operators/associated): `dvd_prod_iff` for `finset` and `finsupp` (#10675)

stuart-presnell committed 4 years ago

a10cb2f3

chore(algebra/algebra/spectrum): move `exists_spectrum_of_is_alg_closed_of_finite_dimensional` (#10919)

j-loreaux committed 4 years ago

a813cf5c

feat(data/polynomial/taylor): taylor_mul (#11193)

pechersky committed 4 years ago

49bf3d3e

feat(data/finset/functor): Functor structures for `finset` (#10980)

YaelDillies committed 4 years ago

a49ee49b

chore(field_theory/ratfunc): comm_ring (ratfunc K) (#11188)

pechersky committed 4 years ago

138c61fc

chore(topology/continuous_on): fix a typo (#11190)

urkud committed 4 years ago

03a54829

feat(ring_theory/algebraic): algebraic functions (#11156)

pechersky committed 4 years ago

3f777613

feat(topology/algebra/ordered): new lemmas, update (#11184)

urkud committed 4 years ago

ebdbe6b0

chore(measure_theory): fix TC assumptions in 2 lemmas (#11185)

urkud committed 4 years ago

02d02dfc

feat(topology/metric_space/basic): add `fin.dist_insert_nth_insert_nth` (#11183)

urkud committed 4 years ago

c1b10417

chore(order/rel_classes): Removed unnecessary `classical` (#11180)

vihdzp committed 4 years ago

6486e9b3

feat(algebraic_geometry/*): The map `F.stalk y ⟶ F.stalk x` for `x ⤳ y` (#11144)

erdOne committed 4 years ago

93cf56c5

feat(linear_algebra/multilinear/basic): the space of multilinear maps is finite-dimensional when the components are finite-dimensional (#10504)

ocfnash committed 4 years ago

892d465a

feat(combinatorics/configuration): Line count equals point count (#11169)

tb65536 committed 4 years ago

53533697

feat(group_theory/specific_groups/*): computes the exponents of the dihedral and generalised quaternion groups (#11166)

Julian-Kuelshammer committed 4 years ago

a6c82afb

feat(data/nat/log): log_mul, log_div (#11164)

pechersky committed 4 years ago

ad76a5ee

feat(algebraic_geometry): The function field of an integral scheme (#11147)

erdOne committed 4 years ago

23b01cc4

feat(normed_space/lp_space): Lp space for `Π i, E i` (#11015)

hrmacbeth committed 4 years ago

1594b0ca

Older