leanprover-community/mathlib3

Pull Requests Commits

feat(analysis/calculus/fderiv_symmetric): prove that the second derivative is symmetric (#8104)

sgouezel committed 4 years ago

f5f8a20f

feat(data/list/duplicate): prop that element is a duplicate (#7824)

pechersky committed 4 years ago

92b64a0d

chore(*): update to lean 3.31.0c (#8122)

gebner committed 4 years ago

5945ca39

chore(algebra/lie/free): tidy up after #8153 (#8163)

ocfnash committed 4 years ago

395d8716

feat(logic/is_empty): add some simp lemmas and unique instances (#7832)

eric-wieser committed 4 years ago

15712902

chore(linear_algebra/matrix/determinant): golf a proof (#8157)

eric-wieser committed 4 years ago

3d2e5ac2

feat(analysis/fourier): span of monomials is dense in C^0 (#8035)

hrmacbeth committed 4 years ago

ca30bd22

feat(algebra/lie/free): construction of free Lie algebras (#8153)

ocfnash committed 4 years ago

3fa61ea4

docs(order/zorn): explain how to use Zorn's lemma (#8125)

YaelDillies committed 4 years ago

4d241724

feat(data/fintype/intervals): fintype instances for set.{Icc,Ioc,Ioo} (#8123)

jcommelin committed 4 years ago

7cbca35f

feat(logic/basic): add two simp lemmas (#8148)

fpvandoorn committed 4 years ago

6e0d2d3b

chore(linear_algebra/matrix/determinant): squeeze some simps for speed up (#8156)

adomani committed 4 years ago

8986c4fd

feat(logic/basic): subtype.subsingleton (#8138)

jcommelin committed 4 years ago

582ee9ee

feat(order/preorder_hom): preorder_hom_eq_id (#8135)

jcommelin committed 4 years ago

aabb900b

feat(category_theory/limits/concrete_category): Some lemmas about limits in concrete categories (#8130)

adamtopaz committed 4 years ago

4a758765

feat(data/int/basic): int.eq_zero_of_div_eq_zero (#8134)

jcommelin committed 4 years ago

2df573a5

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

leanprover-community-bot committed 4 years ago

b9722807

feat(data/int/cast): cast_nat_abs (#8120)

jcommelin committed 4 years ago

0faf0864

feat(topology/vector_bundle): `topological_vector_bundle_core` (#8089)

Nicknamen committed 4 years ago

ad00a021

feat(algebra/free_non_unital_non_assoc_algebra): construction of the free non-unital, non-associative algebra on a type `X` with coefficients in a semiring `R` (#8141)

ocfnash committed 4 years ago

e70093ff

docs(data/string/*): add module docstrings (#8144)

YaelDillies committed 4 years ago

e7131068

feat(algebra/big_operators/basic): nat_abs_sum_le (#8132)

jcommelin committed 4 years ago

8ee29671

feat(data/complex/module): add complex.lift to match zsqrtd.lift (#8107)

eric-wieser committed 4 years ago

3a5851f0

fix(algebra/algebra/subalgebra): fix incorrect namespaces and remove duplicate instance (#8140)

eric-wieser committed 4 years ago

36c90d5e

chore(algebra/algebra): trivial lemmas for alg_equiv (#8139)

eric-wieser committed 4 years ago

d420db54

feat(data/set/basic): range_pair_subset (#8133)

jcommelin committed 4 years ago

9c03c035

feat(algebra/ordered_ring): abs_cases lemma (#8124)

AlexKontorovich committed 4 years ago

1de192f4

feat(linear_algebra/clifford_algebra): two algebras are isomorphic if their quadratic forms are equivalent (#8128)

eric-wieser committed 4 years ago

db059004

docs(data/dlist/basic): add module docstring (#8079)

YaelDillies committed 4 years ago

9a8dcb9b

feat(data/int/basic): int.nat_abs_sub_le (#8118)

jcommelin committed 4 years ago

eeeb2238

Older