leanprover-community/mathlib3

Pull Requests Commits

change "instance" back to "def"

l534zhan committed 4 years ago

Verified a3cebdb3

improved two proofs, changes the "lemmas" that should be "defs" to "instance"

l534zhan committed 4 years ago

Verified 9e0dbd55

Update nonsingular_inverse.lean

l534zhan committed 4 years ago

Verified a8725e76

Update nonsingular_inverse.lean

l534zhan committed 4 years ago

Verified 0a5e3e0c

l534zhan committed 4 years ago

dd0ad12c

feat(category_theory): left-derived functors (#7487)

kim-em committed 4 years ago

531d8504

refactor(measure_theory/simple_func_dense): generalize approximation results from L^1 to L^p (#8114)

hrmacbeth committed 4 years ago

74a0f67b

feat(algebra/invertible): add a missing lemma `inv_of_eq_left_inv` (#8179)

l534zhan committed 4 years ago

a022bb75

feat(group_theory/perm/basic): of_subtype_apply_of_mem (#8174)

pechersky committed 4 years ago

111ac5ca

feat(algebra/periodic): a few more periodicity lemmas (#8062)

benjamindavidson committed 4 years ago

25d042c1

feat(topology/algebra/multilinear): add a linear_equiv version of pi (#8064)

eric-wieser committed 4 years ago

915902e6

docs(data/real/*): add module docstrings (#8145)

YaelDillies committed 4 years ago

edb72b44

feat(data/real/nnreal): cast_nat_abs_eq_nnabs_cast (#8121)

jcommelin committed 4 years ago

10f6c2c4

chore(group_theory/congruence): fix docstring (#8162)

dwarn committed 4 years ago

f8ca7902

fix(topology/continuous_function/basic): fix `continuous_map.id_coe` (#8180)

shingtaklam1324 committed 4 years ago

f5a8b8a6

feat(category_theory/adjunction/fully_faithful): Converses to `unit_is_iso_of_L_fully_faithful` and `counit_is_iso_of_R_fully_faithful` (#8181)

robin-carlier committed 4 years ago

9e9dfc26

feat(data/nat/choose/bounds): exponential bounds on binomial coefficients (#8095)

YaelDillies committed 4 years ago

ea924e57

feat(data/list/cycle): lift next_prev to cycle (#8172)

pechersky committed 4 years ago

67c72b42

chore(algebra/algebra/basic): add `alg_hom.of_linear_map` and lemmas (#8151)

eric-wieser committed 4 years ago

d6a7c3bc

feat(data/equiv/basic): swap_apply_ne_self_iff (#8167)

pechersky committed 4 years ago

dfc42f96

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

Older