leanprover-community/mathlib

Pull Requests Commits

feat(convex) continuity of real convex functions

MaloJaffre committed 3 years ago

4e66c823

feat(algebraic_geometry): Prime spectrum is sober. (#10989)

erdOne committed 3 years ago

f3b380e4

chore(order/*): Change `order_hom` notation (#10988)

YaelDillies committed 3 years ago

086469f7

feat(ring_theory/integral_closure): The product of the leading coeff and the root is integral. (#10807)

erdOne committed 3 years ago

03062ea4

feat(data/list/count): countp of true and false (#10986)

b-mehta committed 3 years ago

2cfa052b

feat(field_theory/adjoin): add dim_bot, finrank_bot (#10964)

Sebastian-Monnet committed 3 years ago

08b13ec9

feat(data/list/count): count_le_length (#10982)

kmill committed 3 years ago

f4e46fd2

feat(order/complete_boolean_algebra): lemmas about binfi (#10852)

b-mehta committed 3 years ago

04779a32

feat(analysis/normed_space/pointwise): more on pointwise operations on sets in normed spaces (#10820)

sgouezel committed 3 years ago

f00007dc

split(data/finset/sigma): Split off `data.finset.basic` (#10957)

YaelDillies committed 3 years ago

e15e015b

feat(data/finset/*): Random lemmas (#10955)

YaelDillies committed 3 years ago

3f164099

split(data/psigma/order): Split off `order.lexicographic` (#10953)

YaelDillies committed 3 years ago

2b9ab3bb

feat(quadratic_form/prod): quadratic forms on product and pi types (#10939)

eric-wieser committed 3 years ago

43159737

feat(group_theory/index): Transitivity of finite relative index. (#10936)

tb65536 committed 3 years ago

c8f0afcd

feat(data/real/ennreal): add monotonicity lemmas for ennreal.to_nnreal (#10556)

kkytola committed 3 years ago

24cefb50

refactor(*): Random lemmas and modifications from the shifting refactor. (#10940)

erdOne committed 3 years ago

c5bb320c

feat(linear_algebra/quadratic_form/basic): `linear_map.comp_quadratic_form` (#10950)

eric-wieser committed 3 years ago

ee25d58a

feat(linear_algebra/eigenspace): the eigenvalues of a linear endomorphism are in its spectrum (#10912)

dupuisf committed 3 years ago

b2e881b9

feat(data/{finset,multiset}/locally_finite): When an `Icc` is a singleton, cardinality generalization (#10925)

YaelDillies committed 3 years ago

12ee59fa

feat(ring_theory/tensor_product): Range of `tensor_product.product_map` (#10882)

tb65536 committed 3 years ago

da07a992

chore(analysis/normed_space/exponential + logic/function/iterate): fix typos in doc-strings (#10968)

adomani committed 3 years ago

dda469d0

chore(*): fix some doc (#10966)

ericrbg committed 3 years ago

7ca68f8e

feat(topology/tietze_extension): Tietze extension theorem (#10701)

urkud committed 3 years ago

af683b11

refactor(ring_theory/derivation): use weaker TC assumptions (#10952)

urkud committed 3 years ago

fc66d88c

feat(linear_algebra/quadratic_form/complex): all non-degenerate quadratic forms over ℂ are equivalent (#10951)

eric-wieser committed 3 years ago

55f575f1

feat(data/nat/prime): `prime.dvd_prod_iff`; golf `mem_list_primes_of_dvd_prod` (#10624)

stuart-presnell committed 3 years ago

b434a0db

chore(group_theory/quotient_group): make pow definitionally equal (#10833)

eric-wieser committed 3 years ago

ca554bee

feat(data/finsupp/basic): add lemma `disjoint_prod_add` (#10799)

stuart-presnell committed 3 years ago

cea1988f

feat(data/mv_polynomial): add `mv_polynomial.linear_map_ext` (#10945)

urkud committed 3 years ago

4aa7ac67

chore(data/nat/digits): Eliminate `finish` (#10947)

stuart-presnell committed 3 years ago

8dafccc1

Older