leanprover-community/mathlib

Pull Requests Commits

Merge branch 'lean-3.4.2' into is-integrally-closed

jcommelin committed 6 years ago

ef04812f

feat(lift): check whether target is proposition (#1767)

fpvandoorn committed 6 years ago

71247ebe

feat(tactic): mk_simp_attribute command that includes doc string (#1763)

robertylewis committed 6 years ago

c1105de1

feat(data/finset): lemmas for folding min and max (#1774)

jcommelin committed 6 years ago

b031290b

feat(lint): avoid Travis error when declarations are renamed (#1771)

robertylewis committed 6 years ago

827e78b1

feat(data/polynomial): monic.as_sum (#1773)

jcommelin committed 6 years ago

866be5f6

feat(set_theory/cardinal): eq_one_iff_subsingleton_and_nonempty (#1770)

jcommelin committed 6 years ago

922a4ebe

jcommelin committed 6 years ago

0196c38d

feat(tactic/lift): automatically handle pi types (#1755)

urkud committed 6 years ago

3266b960

jcommelin committed 6 years ago

de96ccc6

jcommelin committed 6 years ago

6276659e

Merge branch 'monic-as-sum' into is-integrally-closed

jcommelin committed 6 years ago

2d7992d3

feat(data/polynomial): monic.as_sum

jcommelin committed 6 years ago

d74046a6

jcommelin committed 6 years ago

d0ce0dd9

feat(README): add link to Lean Links [skip ci] (#1768)

fpvandoorn committed 6 years ago

89e7f6fd

refactor(topology/algebra): use dot notation in tendsto.add and friends (#1765)

sgouezel committed 6 years ago

3913d303

doc(*): correct bad markdown (#1764)

robertylewis committed 6 years ago

87929bf7

chore(topology/*): dots for continuity proofs (#1762)

PatrickMassot committed 6 years ago

1c4a2966

feat(topology/uniform_space/cauchy): sequentially complete space with a countable basis is complete (#1761)

urkud committed 6 years ago

89fd0883

feat(measure/bochner_integration): dominated convergence theorem (#1757)

Zhouhang Zhou committed 6 years ago

177ccedb

refactor(analysis/calculus/mean_value): prove the mean value theorem using 1D derivative (#1740)

sgouezel committed 6 years ago

8a89b063

refactor(topology/algebra): use the dot notation in `continuous_mul` and friends (#1758)

sgouezel committed 6 years ago

431551a8

chore(scripts/nolint.txt): regenerate

robertylewis committed 6 years ago

a350f034

feat(analysis/complex/exponential): limits of exp (#1744)

sgouezel committed 6 years ago

343c54d6

doc(docs/contribute, meta/expr): sectioning doc strings (#1723)

robertylewis committed 6 years ago

e68b2be5

doc(windows.md): update [ci skip] (#1742)

fpvandoorn committed 6 years ago

b46ef845

feat(analysis/specific_limits): add `cauchy_seq_of_edist_le_geometric` (#1743)

urkud committed 6 years ago

9bb69dca

feat(measure_theory/bochner_integration): linearity of the Bochner Integral (#1745)

Zhouhang Zhou committed 6 years ago

817711d8

chore(topology/instances/ennreal): simplify some statements&proofs (#1750)

urkud committed 6 years ago

65bdbabc

feat(data/real/ennreal): more simp lemmas about `inv` and continuity of `inv` (#1749)

urkud committed 6 years ago

8f11c466

Newer Older