leanprover-community/mathlib3

Pull Requests Commits

refactor(tactic/interactive): remove dependencies of (#878)

cipher1024 committed 6 years ago

00aaf05a

jcommelin committed 6 years ago

Verified 9b3e91b0

refactor(analysis/normed_space): use bundled type for `fderiv` (#956)

jlpaca committed 6 years ago

53f98786

fix(README): update maintainer list

PatrickMassot committed 6 years ago

Verified b49bf61c

feat(data/equiv/basic): sum_compl_apply and others (#961)

ChrisHughes24 committed 6 years ago

Verified 0444f9c2

refactor(analysis/normed_space/operator_norm): replace subspace with … (#955)

sgouezel committed 6 years ago

038f809c

feat(function/embedding): ext and ext_iff (#962)

ChrisHughes24 committed 6 years ago

1d9ff681

fix(ring_theory/adjoin_root): move adjoin_root out of adjoin_root namespace (#960)

ChrisHughes24 committed 6 years ago

0d7b4195

refactor(data/equiv/basic): simplify definition of equiv.set.range (#959)

ChrisHughes24 committed 6 years ago

45456cf1

feat(data/list/basic): index_of_inj (#954)

ChrisHughes24 committed 6 years ago

63bbd1c3

fix(tactic/interactive): allow `convert e using 0`

digama0 committed 6 years ago

3478f1f6

feat(tactic/clear_except): clear most of the assumptions in context (#957)

cipher1024 committed 6 years ago

Verified 9daa1a57

feat(data/[fin]set): add some more basic properties of (finite) sets (#948)

fpvandoorn committed 6 years ago

4b9d94dc

feat(tactic/linarith): treat expr atoms up to defeq (#950)

robertylewis committed 6 years ago

Verified 7370cbf2

fix(topology/order): Missing Prop annotation (#952)

PatrickMassot committed 6 years ago

784a68c3

feat(tactic/ring): treat expr atoms up to defeq (#949)

digama0 committed 6 years ago

e4fc5afd

style(tactic/omega): whitespace and minor tweaks

digama0 committed 6 years ago

c1aff1b5

feat(group_theory/subgroup): additive version of inj_iff_trivial_ker (#947)

ramonfmir committed 6 years ago

d0140dd8

feat(analysis/normed_space): more facts about operator norm (#927)

jlpaca committed 6 years ago

032400bd

feat(scripts): use apt-get on ubuntu and support older Python versions (#945)

cipher1024 committed 6 years ago

Verified 8b23dadc

feat(tactic/omega): tactic for linear integer & natural number arithmetic (#827)

skbaek committed 6 years ago

3f4b154a

fix(test/local_cache): make the trace text explicit and quiet (#941)

khoek committed 6 years ago

4b8106b3

feat(*): various additions to low-level files (#904)

fpvandoorn committed 6 years ago

7bbbee1e

feat(data/finset): powerset_len (subsets of a given size) (#899)

digama0 committed 6 years ago

22948763

feat(data/set/intervals): some interval lemmas (#942)

kim-em committed 6 years ago

8985a433

feature(category_theory/instances/Top/open[_nhds]): category of open sets, and open neighbourhoods of a point (merge #920 first) (#922)

kim-em committed 6 years ago

361e2163

feat(nat/basic): add some basic nat inequality lemmas (#937)

aarondroidbryce committed 6 years ago

5f04e76e

feat(topology/algebra/continuous_functions): the ring of continuous functions (#923)

kim-em committed 6 years ago

d06eb858

feat(scripts): disable testing the install scripts in external PRs (#936)

cipher1024 committed 6 years ago

Verified ca5d4c1f

fix(algebra/big_operators): change variables in finset.prod_map to remove spurious [comm_monoid β] (#934)

NeilStrickland committed 6 years ago

a1b7dcdf

Newer Older