leanprover-community/mathlib

Pull Requests Commits

add docs, minor edits

alreadydone committed 3 years ago

0d44e30e

alreadydone committed 3 years ago

1108a969

alreadydone committed 3 years ago

48462c42

move to eq_to_hom, rename

alreadydone committed 3 years ago

30cfcc45

alreadydone committed 3 years ago

9467a6e2

unnecessary lemma

alreadydone committed 3 years ago

d87fb511

minimalistic proof

alreadydone committed 3 years ago

249126d8

naturality of normalize

alreadydone committed 3 years ago

12fd940d

alreadydone committed 3 years ago

ff09a069

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

Older