leanprover-community/mathlib3

Pull Requests Commits

chore(opposites): merge two definitions of `opposite` (#1036)

Yury G. Kudryashov committed 6 years ago

96ea9b99

feat(data/nat/basic): make decreasing induction eliminate to Sort (#1032)

fpvandoorn committed 6 years ago

def48b06

fix(data/nat/enat): Fix typo in lemma name (#1037)

jcommelin committed 6 years ago

ad0f42df

chore(*): reduce imports (#1033)

kim-em committed 6 years ago

c75c096a

feat(category_theory): monos and epis in Type and Top (#1030)

rwbarton committed 6 years ago

b5aae18a

refactor(topology): change continuous_at_within to continuous_within_at (#1034)

sgouezel committed 6 years ago

136e67a6

feat(tactic/terminal_goal): determine if other goals depend on the current one (#984)

kim-em committed 6 years ago

3022cafd

feat(category_theory): adjoint equivalences and limits under equivalences (#986)

fpvandoorn committed 6 years ago

7b579b79

feat(data/nat/basic): decreasing induction (#1031)

sgouezel committed 6 years ago

ae8f197b

feat(data/equiv/functor): map_equiv (#1026)

jcommelin committed 6 years ago

e7b64c55

fix(docs/tactics): fix layout, remove noise

PatrickMassot committed 6 years ago

Verified 02857d56

feat(tactic): new tactics to normalize casts inside expressions (#988)

Paul-Nicolas Madelaine committed 6 years ago

22790e06

fix(data/multiset): remove duplicate setoid instance (#1027)

jcommelin committed 6 years ago

fe19bdb4

feat(analysis/normed_space/deriv): more material on derivatives (#966)

sgouezel committed 6 years ago

ade99c8c

squeeze_simp (#1019)

kim-em committed 6 years ago

a72641be

feat(category_theory/opposites): iso.op (#1021)

rwbarton committed 6 years ago

cefb9d43

feat(algebra/order_functions): generalize strict_mono.monotone (#1022)

rwbarton committed 6 years ago

6dc06824

feat(topology/constructions): topology of sum types (#1016)

rwbarton committed 6 years ago

07ba43ee

feat(data/equiv/basic): equiv.nonempty_iff_nonempty (#1020)

rwbarton committed 6 years ago

f8385b19

feat(tactics/interactive): choose uses exists_prop (#1014)

PatrickMassot committed 6 years ago

01b345c1

feat(category_theory/products): missing simp lemmas (#1003)

kim-em committed 6 years ago

c8a0bb6b

feat(category_theory/iso): missing lemmas (#1001)

kim-em committed 6 years ago

6c35df0d

document the change in scripts (#1024)

cipher1024 committed 6 years ago

82f151f5

feat(Top.presheaf_ℂ): presheaves of functions to topological commutative rings (#976)

kim-em committed 6 years ago

70cd00bc

chore(Github): no need to wait for Appveyor anymopre

cipher1024 committed 6 years ago

Verified b9b5bb4b

chore(scripts): migrate scripts to own repo (#1011)

cipher1024 committed 6 years ago

e42d808b

feat(category_theory): lemmas about cancellation (#1005)

kim-em committed 6 years ago

Verified 48645152

feat(topology/maps): closed embeddings (#1013)

rwbarton committed 6 years ago

1e0761e5

feat(logic/function): comp₂ -- useful for binary operations (#993)

jcommelin committed 6 years ago

de5d0387

fix(docs/*): docs reorganization [skip ci] (#1012)

PatrickMassot committed 6 years ago

a154dedc

Newer Older