leanprover-community/mathlib3

Pull Requests Commits

Remove code that belonged to other PRs

jcommelin committed 6 years ago

6f5ee17b

Merge branch 'lean-3.4.2' into gen-fun

jcommelin committed 6 years ago

07ca5742

Cleanup after merged PRs

jcommelin committed 6 years ago

2dac1848

Merge branch 'lean-3.4.2' into gen-fun

jcommelin committed 6 years ago

edbc84d6

Analogue for mv_power_series

jcommelin committed 6 years ago

28f3a095

refactor(topology/metric_space/emetric_space): redefine `diam` (#1941)

urkud committed 6 years ago

Verified a3421322

feat(algebra/pointwise): pointwise scalar-multiplication lemmas (#1925)

jlpaca committed 6 years ago

Verified 1843bfc9

feat(data/set/basic): define `set.subsingleton` (#1939)

urkud committed 6 years ago

Verified 58899d43

chore(data/subtype): fix `∀` vs `Π` (#1940)

urkud committed 6 years ago

Verified bacd4da5

feat(data/fintype): range_prod_eq_univ_prod (#1937)

jcommelin committed 6 years ago

Verified 11b94970

Some updates after PRs

jcommelin committed 6 years ago

9b6f9778

feat(data/nat/basic): two identities for `choose` (#1936)

jcommelin committed 6 years ago

Verified 6e6e6da6

Update units.lean (#1938)

jcommelin committed 6 years ago

Verified a500c24c

fix(data/nat/basic): make arguments to `choose_succ_right_eq` explicit (#1935)

jcommelin committed 6 years ago

Verified 50bbb8df

Finished sum_bernoulli

jcommelin committed 6 years ago

19dfd9d6

Playing with Bernoulli

jcommelin committed 6 years ago

a9953878

feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices. (#1913)

Oliver Nash committed 6 years ago

Verified 5ce0c0a2

chore(scripts/nolints): regenerate

robertylewis committed 6 years ago

ddba2aea

feat(analysis/convex): define convex hull (#1915)

urkud committed 6 years ago

Verified a8ba81b3

Small start on generating functions

jcommelin committed 6 years ago

ddcb8efa

chore(ci): remove unused olean-rs setup from build (#1932)

robertylewis committed 6 years ago

Verified cae9cc97

feat(ci): build and push html documentation (#1927)

robertylewis committed 6 years ago

Verified 80f5bd54

fix(data/set/finite): finite.fintype is a def (#1931)

kbuzzard committed 6 years ago

Verified 4c2d6787

fix(tactic/scc): detect Props (#1930)

digama0 committed 6 years ago

Verified b7e5f75f

feat(tactic/use): apply exists_prop after use (#1882)

PatrickMassot committed 6 years ago

Verified 1bd23bf1

fix(tactic/squeeze): compatibility with `simp [<-...]` (#1923)

Vierkantor committed 6 years ago

Verified dcbc719b

fix(tactic/finish): fix one classical leak, document another (#1929)

avigad committed 6 years ago

Verified 9bc01784

feat(data/W): show finitely branching W types are encodable (#1817)

avigad committed 6 years ago

Verified 868333b9

chore(category_theory): use the new @[ext] attribute on structures (#1663)

kim-em committed 6 years ago

Verified 4ac87ab5

chore(*): add inhabited instances (#1898)

gebner committed 6 years ago

Verified 4aa3eee4

Older