leanprover-community/mathlib

Pull Requests Commits

feat(algebra/*,data/real/*): add some inequalities about `canonically_ordered_comm_semiring`s (#1746)

urkud committed 6 years ago

1b3347df

chore(data/finset,order/filter): simplify a few proofs (#1747)

urkud committed 6 years ago

8e74c62a

feat(analysis/complex/exponential): derivatives (#1695)

sgouezel committed 6 years ago

198fb09d

feat(topology/algebra/infinite_sum): prove `cauchy_seq_of_edist_le_of_summable` (#1739)

urkud committed 6 years ago

01b1576c

feat(data/nat/multiplicity): multiplicity_choose and others (#1704)

ChrisHughes24 committed 6 years ago

255bebc0

feat(analysis/complex/basic): restriction of scalars, real differentiability of complex functions (#1716)

sgouezel committed 6 years ago

3443a7d4

feat(order/conditionally_complete_lattice): with_top (with_bot L) ins… (#1725)

kbuzzard committed 6 years ago

33df7e88

chore(data/nat/basic): add some docs, drop unused arguments (#1741)

urkud committed 6 years ago

ef47de41

feat(topology/metric_space/basic): define `cauchy_seq_of_le_tendsto_0` (#1738)

urkud committed 6 years ago

73735ad0

feat(measure_theory/bochner_integration): bochner integral of simple functions (#1676)

Zhouhang Zhou committed 6 years ago

242159f8

feat(topology/algebra/infinite_sum): add `has_sum` versions of a few `tsum` lemmas (#1737)

urkud committed 6 years ago

6af35ecb

feat(order/filter/basic): add more lemmas about `tendsto _ _ at_top` (#1713)

urkud committed 6 years ago

bf509d78

chore(topology/metric_space/emetric_space): define `edist_le_zero` (#1735)

urkud committed 6 years ago

a03a0720

feat(algebra/group): define `mul/add_left/right_injective` (#1730)

urkud committed 6 years ago

13fedc15

feat(topology/metric_space/emetric_space): polygonal inequalities (#1736)

urkud committed 6 years ago

7b1cdd4f

feat(data/real/ennreal): 3 simple lemmas (#1734)

urkud committed 6 years ago

ca53b5d5

feat(analysis/normed_space): prove more lemmas, rename some old lemmas (#1733)

urkud committed 6 years ago

2d54a70a

feat(algebra/ordered_*): add three simple lemmas (#1731)

urkud committed 6 years ago

f95c01e4

fix(*): lower instance priority (#1724)

fpvandoorn committed 6 years ago

f86abc77

feat(README) Point users to the tutorial project (#1728)

kbuzzard committed 6 years ago

2b3eaa83

fix(docs/install/project) compiling is quick (#1727)

kbuzzard committed 6 years ago

013e9141

doc(topology/metric_space,measure_theory): move text in copyright docs to module docs (#1726)

robertylewis committed 6 years ago

62c1bc5b

docs(README): revert 96ebf8cc

robertylewis committed 6 years ago

5a1a4698

feat(data/nat): two lemmas about choose (#1717)

b-mehta committed 6 years ago

004618ad

fix(tactic/ext): handle case where goal is solved early (#1721)

robertylewis committed 6 years ago

58fc8301

feat(data/finset): add cardinality of map (#1722)

b-mehta committed 6 years ago

a13027a5

add div_le_div_iff (#1720)

b-mehta committed 6 years ago

faf32899

make set_of_eq_eq_singleton a simp lemma (#1719)

alexjbest committed 6 years ago

af9dcb98

feat(group_theory/congruence): quotients of monoids by congruence relations (#1710)

101damnations committed 6 years ago

9d031be0

refactor(topology/metric_space/lipschitz): review API of `lipschitz_with` (#1700)

urkud committed 6 years ago

f34bb6b9

Newer Older