leanprover-community/mathlib

Pull Requests Commits

feat(measure_theory/set_integral): integrals over subsets (#1875)

Zhouhang Zhou committed 6 years ago

aa6cc06f

refactor(algebra/char_zero): use `function.injective` (#1894)

urkud committed 6 years ago

217b5e72

feat(*): assorted simple lemmas, simplify some proofs (#1895)

urkud committed 6 years ago

f3835fab

feat(data/bool): coe_bool_iff (#1891)

digama0 committed 6 years ago

d32c7977

chore(ring_theory/polynomial): remove decidable_eq assumptions (#1890)

ChrisHughes24 committed 6 years ago

d548d92e

feat(measure_theory/bochner_integration): dominated convergence theorem for filters (#1884)

Zhouhang Zhou committed 6 years ago

c8ae79d0

feat(geometry/manifold/mfderiv): derivative of functions between smooth manifolds (#1872)

sgouezel committed 6 years ago

9ac26cb6

feat(logic/basic): forall_or_distrib (#1887)

digama0 committed 6 years ago

4f81942d

chore(order/filter/*): use `s ∈ f` instead of `s ∈ f.sets` (#1885)

urkud committed 6 years ago

58610ffd

feat(analysis/calculus/tangent_cone): define and use `tangent_cone_congr` (#1886)

urkud committed 6 years ago

05457fdd

chore(*): use `ne_` instead of `neq_` in lemma names (#1878)

urkud committed 6 years ago

b3ed6e61

docs(README): add new maintainers (#1881)

jcommelin committed 6 years ago

8e70388a

feat(linear_algebra/tensor_product): tensor product right identity (#1880)

Oliver Nash committed 6 years ago

d6147362

refactor(order/lattice): generalize `directed_of_mono` (#1879)

urkud committed 6 years ago

819939fb

chore(data/set/lattice): use `∃ x ∈ s` instead of `∃ x, x ∈ s ∧` in `mem_bUnion_iff` (#1877)

urkud committed 6 years ago

9f7ae9ab

fix doc strings (#1876)

Zhouhang Zhou committed 6 years ago

416b7d87

feat(analysis/ODE/gronwall): A version of Grönwall's inequality (#1846)

urkud committed 6 years ago

e095e306

feat(topology/algebra/ordered): add order topology for partial orders… (#1276)

kappelmann committed 6 years ago

c5d91bc7

chore(measure_theory/bochner_integration): make proofs shorter (#1871)

Zhouhang Zhou committed 6 years ago

25dded2d

chore(algebra/module): add some missing `*_cast` tags (#1863)

urkud committed 6 years ago

f67df78c

refactor(docs): additions, modifications, reorganization (#1815)

robertylewis committed 6 years ago

ff2a41e4

refactor(data/set/basic): change def of `⊂` to match `<` (#1862)

urkud committed 6 years ago

baa3aa73

feat(linear_algebra/multilinear): basics of multilinear maps (#1814)

sgouezel committed 6 years ago

d7cebcf6

docs(tactic/tauto): elaborate tauto docs [ci skip] (#1869)

PatrickMassot committed 6 years ago

39c10cdb

feat(analysis/calculus/mean_value): add generalized "fencing" inequality (#1838)

urkud committed 6 years ago

52899945

docs(tactics): tautology (#1860)

FredericLeRoux committed 6 years ago

9afc6f2f

refactor(analysis/asymptotics): introduce `is_O_with` (#1857)

urkud committed 6 years ago

92841c2e

chore(order/zorn): add docstrings, drop `chain.directed` (#1861)

urkud committed 6 years ago

69e07e25

feat(topology/maps): a few lemmas about `is_open_map` (#1855)

urkud committed 6 years ago

a1b73125

chore(*): various simple lemmas about `*_equiv`, add missing attrs (#1854)

urkud committed 6 years ago

15c434a2

Newer Older