Commits leanprover-community/mathlib3

wip

b-mehta committed 4 years ago

Verified 6f78dbe9

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

sgouezel committed 4 years ago

f00007dc

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

YaelDillies committed 4 years ago

e15e015b

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

YaelDillies committed 4 years ago

3f164099

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

YaelDillies committed 4 years ago

2b9ab3bb

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

eric-wieser committed 4 years ago

43159737

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

tb65536 committed 4 years ago

c8f0afcd

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

kkytola committed 4 years ago

24cefb50

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

erdOne committed 4 years ago

c5bb320c

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

eric-wieser committed 4 years ago

ee25d58a

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

dupuisf committed 4 years ago

b2e881b9

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

YaelDillies committed 4 years ago

12ee59fa

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

tb65536 committed 4 years ago

da07a992

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

adomani committed 4 years ago

dda469d0

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

ericrbg committed 4 years ago

7ca68f8e

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

urkud committed 4 years ago

af683b11

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

urkud committed 4 years ago

fc66d88c

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

eric-wieser committed 4 years ago

55f575f1

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

stuart-presnell committed 4 years ago

b434a0db

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

eric-wieser committed 4 years ago

ca554bee

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

stuart-presnell committed 4 years ago

cea1988f

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

urkud committed 4 years ago

4aa7ac67

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

stuart-presnell committed 4 years ago

8dafccc1

feat(algebra/module/submodule_lattice, linear_algebra/projection): two lemmas about `is_compl` (#10709)

ADedecker committed 4 years ago

7e48e350

refactor(linear_algebra/sesquilinear_form): Use similar definition as used in `bilinear_map` (#10443)

mcdoll committed 4 years ago

a6b2f94a

feat(order/galois_connection, linear_algebra/basic): `x ∈ R ∙ y` is a transitive relation (#10943)

ADedecker committed 4 years ago

d5653736

feat(order/monovary): Monovariance of a pair of functions. (#10890)

YaelDillies committed 4 years ago

2ceda785

chore(combinatorics/simple_graph/basic): Golf and cleanup (#10942)

YaelDillies committed 4 years ago

d145e8e3

feat(analysis/special_functions/non_integrable): examples of non-integrable functions (#10788)

urkud committed 4 years ago

5ac4cd35

feat(algebra/algebra/subalgebra): define the center of a (unital) algebra (#10910)

ocfnash committed 4 years ago

c88943fa