leanprover-community/mathlib3

Pull Requests Commits

feat(topology/category/Top): nonempty inverse limit of compact Hausdorff spaces (#6271)

kmill committed 4 years ago

d4ef2e85

feat(data/set/finite): complement of finite set is infinite (#6266)

kbuzzard committed 4 years ago

bf9ca8b5

feat(option/basic): add join_eq_none (#6269)

fpvandoorn committed 4 years ago

7a7a5591

feat(data/real/liouville, ring_theory/algebraic): a Liouville number is transcendental! (#6204)

adomani committed 4 years ago

781cc63f

feat(algebra/category/Module): the free/forgetful adjunction for R-modules (#6168)

kim-em committed 4 years ago

efa6877b

feat(algebra/algebra,linear_algebra): add *_equiv.of_left_inverse (#6167)

eric-wieser committed 4 years ago

3bf72416

chore(topology/basic): add `continuous_at_congr` and `continuous_at.congr` (#6267)

urkud committed 4 years ago

2289b185

doc(*): remove `\\` hack for latex backslashes in markdown (#6263)

robertylewis committed 4 years ago

0b4823cc

doc(algebraic_geometry/structure_sheaf): fix latex (#6262)

robertylewis committed 4 years ago

16eb4af7

feat(analysis/special_functions): strict differentiability of `real.exp` and `real.log` (#6256)

urkud committed 4 years ago

7459c21c

feat(analysis/special_functions): `sqrt` is infinitely smooth at `x ≠ 0` (#6255)

urkud committed 4 years ago

b0071f3f

feat(topology/algebra/normed_group): completion of normed groups (#6189)

jcommelin committed 4 years ago

8a431630

chore(linear_algebra/dfinsupp): make lsum a linear_equiv (#6185)

eric-wieser committed 4 years ago

35c070fa

doc(algebra/big_operators): fix formatting of library note (#6261)

robertylewis committed 4 years ago

2411d681

chore(data/equiv/basic): add lemmas about `equiv.cast` (#6246)

eric-wieser committed 4 years ago

362619eb

doc(control/fold): fix bad markdown (#6245)

robertylewis committed 4 years ago

841b0074

doc(topology/category/*): 5 module docs (#6240)

Julian-Kuelshammer committed 4 years ago

beee5d86

feat(data/set/intervals/basic): not_mem of various intervals (#6238)

benjamindavidson committed 4 years ago

0716fa44

feat(order/well_founded_set): finite antidiagonal of well-founded sets (#6208)

awainverse committed 4 years ago

914517b5

feat(analysis/normed_space/operator_norm): bundle more arguments (#6207)

urkud committed 4 years ago

1a438889

chore(linear_algebra/finsupp): make lsum a linear_equiv (#6183)

eric-wieser committed 4 years ago

8d9eb266

feat(ring_theory/finiteness): add quotient of finitely presented (#6098)

riccardobrasca committed 4 years ago

314f5ad7

feat(apply_fun): handle implicit arguments (#6091)

kim-em committed 4 years ago

3cec1cf6

feat(number_theory/bernoulli): the odd Bernoulli numbers (greater than 1) are zero (#6056)

laughinggas committed 4 years ago

d3c56678

feat(data/equiv): Add lemmas to reduce `@finset.univ (perm (fin n.succ)) _` (#5593)

eric-wieser committed 4 years ago

2da1ab41

feat(category/limits/shapes/zero): lemmas about is_isomorphic 0 (#6251)

kim-em committed 4 years ago

dc917df7

feat(algebra/category/Module): allow writing (0 : Module R) (#6249)

kim-em committed 4 years ago

d7003c1d

feat(topology/connected.lean): define pi_0 and prove basic properties (#6188)

callesonne committed 4 years ago

2961e79c

docs(algebraic_geometry/Scheme): fix typo in module docstring (#6254)

jcommelin committed 4 years ago

acf2b6d8

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

leanprover-community-bot committed 4 years ago

dbe586c1

Newer Older