leanprover-community/mathlib3

Pull Requests Commits

feat(measure_theory/giry_monad): dirac_bind_comp

digama0 committed 6 years ago

a897bd68

feat(tactic/squeeze): remove noise from output (#1047)

cipher1024 committed 6 years ago

Verified 73c3f717

refactor(data/complex/exponential): improve trig proofs (#1041)

digama0 committed 6 years ago

fa0e7570

feat(adjointify): make definition easier for elaborator (#1045)

fpvandoorn committed 6 years ago

5e5298b9

fix(topology/stone_cech): faster proof from @PatrickMassot (#1042)

rwbarton committed 6 years ago

45afa86e

feat(set_theory/surreal): surreal numbers (#958)

digama0 committed 6 years ago

901178e2

refactor: change variables order in some composition lemmas (#1035)

sgouezel committed 6 years ago

0b350228

feat(tactic/basic): add tactic.rewrite, and sort list (#1039)

jcommelin committed 6 years ago

f633c948

fix(data/complex/exponential): make complex.exp irreducible (#1040)

robertylewis committed 6 years ago

a6c1f377

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

Older