leanprover-community/mathlib3

Pull Requests Commits

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

eric-wieser committed 5 years ago

362619eb

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

robertylewis committed 5 years ago

841b0074

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

Julian-Kuelshammer committed 5 years ago

beee5d86

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

benjamindavidson committed 5 years ago

0716fa44

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

awainverse committed 5 years ago

914517b5

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

urkud committed 5 years ago

1a438889

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

eric-wieser committed 5 years ago

8d9eb266

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

riccardobrasca committed 5 years ago

314f5ad7

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

kim-em committed 5 years ago

3cec1cf6

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

laughinggas committed 5 years ago

d3c56678

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

eric-wieser committed 5 years ago

2da1ab41

Merge remote-tracking branch 'origin/master' into connective

kim-em committed 5 years ago

d94981f2

cleanup and lint

kim-em committed 5 years ago

d024a81e

kim-em committed 5 years ago

096bd435

Merge branch 'int_lemmas' into connective

kim-em committed 5 years ago

4623287f

kim-em committed 5 years ago

cb99c2bf

kim-em committed 5 years ago

99a66d8a

Merge branch 'int_lemmas' into connective

kim-em committed 5 years ago

6f7aaf7d

kim-em committed 5 years ago

1df86598

kim-em committed 5 years ago

6d8f8d0f

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

kim-em committed 5 years ago

dc917df7

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

kim-em committed 5 years ago

d7003c1d

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

callesonne committed 5 years ago

2961e79c

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

jcommelin committed 5 years ago

acf2b6d8

kim-em committed 5 years ago

d79affc3

kim-em committed 5 years ago

b5ef9de8

kim-em committed 5 years ago

d595d652

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

leanprover-community-bot committed 5 years ago

dbe586c1

kim-em committed 5 years ago

58d6d32a

kim-em committed 5 years ago

8f39f001

Newer Older