leanprover-community/mathlib

Pull Requests Commits

alreadydone committed 3 years ago

73fcaf3d

yuma-mizuno committed 3 years ago

20fd0c77

yuma-mizuno committed 3 years ago

f7bf7c17

yuma-mizuno committed 3 years ago

1b16260a

adjust priority

yuma-mizuno committed 3 years ago

fd492ff6

yuma-mizuno committed 3 years ago

48e42ced

yuma-mizuno committed 3 years ago

f6ae248d

remove unused lemmas

yuma-mizuno committed 3 years ago

f187eeaa

yuma-mizuno committed 3 years ago

26ef7514

coherence theorem

yuma-mizuno committed 3 years ago

167fa1f7

feat(topology/uniform_space/cauchy): add a few lemmas (#11912)

urkud committed 3 years ago

352e0642

feat(topology): a few more results about compact sets (#11905)

fpvandoorn committed 3 years ago

2b9aca75

feat(set_theory/ordinal_arithmetic): `le_one_iff` (#11847)

vihdzp committed 3 years ago

b8fb8e5b

feat(algebra.group.hom_instances): Define left and right multiplication operators (#11843)

mans0954 committed 3 years ago

2726e238

feat(order): some properties about monotone predicates (#11904)

fpvandoorn committed 3 years ago

5008de8b

feat(order/filter/basic): add lemma `le_prod_map_fst_snd` (#11901)

berndlosert committed 3 years ago

d3cdcd83

chore(data/pi): add pi.prod and use elsewhere (#11877)

eric-wieser committed 3 years ago

9648ce29

feat(order/atoms): finite orders are (co)atomic (#11930)

nomeata committed 3 years ago

ca2450fe

chore(algebra/tropical/basic): remove 3 instances (#11920)

adomani committed 3 years ago

c8827532

chore(data/fintype/basic): documenting elaboration bug (#11247)

kmill committed 3 years ago

fea68aac

refactor(algebra/ring/basic): rename lemmas about `a*(-b)` and `(-a)*b` (#11925)

eric-wieser committed 3 years ago

3aa5b8a9

feat(data/complex/basic): re-im set product (#11770)

urkud committed 3 years ago

4e17e081

feat(category_theory/pseudoabelian/basic): basic facts and contructions about pseudoabelian categories (#11817)

joelriou committed 3 years ago

78c39752

feat(analysis/normed_space/basic): add lemmas `nnnorm_mul_le` and `nnnorm_pow_succ_le` (#11915)

j-loreaux committed 3 years ago

56db7ed0

feat(topology/algebra/uniform_group): `cauchy_seq.const_mul` and friends (#11917)

ecstatic-morse committed 3 years ago

a3d6b43c

feat(model_theory/substructures): More operations on substructures (#11906)

awainverse committed 3 years ago

4545e31e

chore(*): update to lean 3.39.1c (#11926)

gebner committed 3 years ago

1ae83049

chore(algebra/order/ring): add a few aliases (#11911)

urkud committed 3 years ago

b1269b0d

feat(*): localized `R[X]` notation for `polynomial R` (#11895)

pechersky committed 3 years ago

85d9f218

feat(group_theory/submonoid/operations): prod_le_iff and le_prod_iff, also for groups and modules (#11898)

nomeata committed 3 years ago

59325814

Older