leanprover-community/mathlib

Pull Requests Commits

feat(measure_theory/decomposition/radon_nikodym): Radon-Nikodym and Lebesgue decomposition for signed measures (#9065)

kex-y committed 4 years ago

420f11ab

refactor(data/real/ereal): replace `.cases` with `.rec` (#9321)

eric-wieser committed 4 years ago

c4fbb6ff

chore(group_theory/order_of_element): bump up (#9318)

ericrbg committed 4 years ago

30617c7b

feat(data/finset): add lemmas (#9209)

urkud committed 4 years ago

b5a6422f

refactor(data/polynomial/{coeff,monomial}): move smul_eq_C_mul (#9287)

BoltonBailey committed 4 years ago

524ded6c

feat(measure_theory/measure/vector_measure): add `mutually_singular.neg` (#9282)

kex-y committed 4 years ago

4cee7438

feat(topology/continuous_function/basic): gluing lemmas (#9239)

hrmacbeth committed 4 years ago

78340e39

feat(topology/bases): continuous_of_basis_is_open_preimage (#9281)

justus-springer committed 4 years ago

49e0bcfe

chore(scripts): update nolints.txt (#9317)

leanprover-community-bot committed 4 years ago

13780bce

feat(data/vector/basic): lemmas, and linting (#9260)

kim-em committed 4 years ago

46ff4496

refactor(analysis/convex/{extreme, exposed}): generalize `is_extreme` and `is_exposed` to semimodules (#9264)

YaelDillies committed 4 years ago

175afa8a

chore(ring_theory/polynomial/tower): remove a duplicate instance (#9302)

eric-wieser committed 4 years ago

ae726e10

feat(algebra/algebra/basic): lemmas about alg_hom and scalar towers (#9249)

ChrisHughes24 committed 4 years ago

c2d8a58d

fix(data/dfinsupp): fix nat- and int- module diamonds (#9299)

eric-wieser committed 4 years ago

866294d3

chore(data/real/pi): split into three files (#9295)

kim-em committed 4 years ago

3703ab2a

feat(ci): Download all possible caches in gitpod (#9286)

eric-wieser committed 4 years ago

8c96c549

feat(field_theory/algebraic_closure): any two algebraic closures are isomorphic (#9231)

ChrisHughes24 committed 4 years ago

72a8cd68

feat(docker): pin version for better reproducibility (#9304)

alexjbest committed 4 years ago

cb33f68d

feat(topology/instances/ennreal): sum of nonzero constants is infinity (#9294)

sgouezel committed 4 years ago

4df2a1bf

chore(group_theory/submonoid/operations): split a file (#9292)

kim-em committed 4 years ago

e41e9bce

feat(linear_algebra/matrix/to_lin): simp lemmas for to_matrix and algebra (#9267)

ChrisHughes24 committed 4 years ago

7389a6b1

feat(algebra/pointwise): more lemmas about pointwise actions (#9226)

eric-wieser committed 4 years ago

ba282349

chore(analysis/normed_space/finite_dimensional): restructure imports (#9289)

kim-em committed 4 years ago

e29dfc19

feat(data/vector/basic): induction principles (#9261)

kim-em committed 4 years ago

d93c6a85

chore(scripts): update nolints.txt (#9290)

leanprover-community-bot committed 4 years ago

238d7927

refactor(field_theory/algebraic_closure): Move construction of algebraic closure and lemmas about alg closed fields into seperate files. (#9265)

ChrisHughes24 committed 4 years ago

035bd249

feat(linear_algebra/{multilinear,alternating): add of_subsingleton (#9196)

eric-wieser committed 4 years ago

acb10a55

feat(data/{multiset,finset}/basic): card_erase_eq_ite (#9185)

BoltonBailey committed 4 years ago

976b261a

feat(order/lattice): `sup`/`inf`/`max`/`min` of mono functions (#9284)

urkud committed 4 years ago

f37f57dc

chore(measure_theory/function/simple_func_dense): distance to `approx_on` is antitone (#9271)

urkud committed 4 years ago

4887f80c

Newer Older