leanprover-community/mathlib

Pull Requests Commits

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

leanprover-community-bot committed 4 years ago

793a598b

feat(data/multiset/basic): add lemma that `multiset.map f` preserves `count` under certain assumptions on `f` (#9117)

Paul-Lez committed 4 years ago

98665267

Merge branch 'master' of https://github.com/leanprover-community/mathlib into JasonKYi/lintegral_with_density_eq

kex-y committed 4 years ago

d27559c6

Merge branch 'master' of https://github.com/leanprover-community/mathlib into JasonKYi/pdf

kex-y committed 4 years ago

ff676509

feat(measure_theory/integral/lebesgue): lintegral is strictly monotone under some conditions (#9373)

kex-y committed 4 years ago

168806c0

feat(measure_theory/function/l1_space): add integrability lemma for `measure.with_density` (#9367)

kex-y committed 4 years ago

eba2b2e6

change ae_neq to neq

kex-y committed 4 years ago

a38718ef

make `has_pdf` to require measurability

kex-y committed 4 years ago

1a5e2dd3

add Remy's lemmas + golf

kex-y committed 4 years ago

5c0518fd

kex-y committed 4 years ago

44974958

remove extra line

kex-y committed 4 years ago

884fbf1d

kex-y committed 4 years ago

3d22c415

more generalize

kex-y committed 4 years ago

bd79e9ba

kex-y committed 4 years ago

fe99fe59

refactor(topology/compact_open): use bundled continuous maps (#9351)

kim-em committed 4 years ago

6ea81683

refactor(analysis/inner_product_space/*): split big file (#9382)

hrmacbeth committed 4 years ago

51ad06e5

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

leanprover-community-bot committed 4 years ago

55d8cd0a

feat(data/polynomial/eval): map_equiv (#9375)

ChrisHughes24 committed 4 years ago

42d82435

feat(algebra/group/to_additive): customize the relevant argument (#9138)

fpvandoorn committed 4 years ago

59b9ebb1

chore(analysis/complex/basic): rename `complex/normed_space` (#9366)

eric-wieser committed 4 years ago

64b794a0

chore(algebra/group): move is_unit.inv lemmas (#9364)

pechersky committed 4 years ago

b0cd1f9c

chore(data/pi): add missing `pi.{inv,neg}_def` (#9361)

eric-wieser committed 4 years ago

c42aaa3d

feat(group_theory/*/pointwise): Copy set lemmas about pointwise actions to subgroups and submonoids (#9359)

eric-wieser committed 4 years ago

8ff756cb

chore(measure_theory/integral/interval_integral): generalize `integral_smul` (#9355)

urkud committed 4 years ago

18f06ecf

chore(linear_algebra/basic): add `linear_map.neg_comp`, generalize `linear_map.{sub,smul}_comp` (#9335)

eric-wieser committed 4 years ago

7cb72461

chore(linear_algebra/basic): split out quotients and isomorphism theorems (#9332)

kim-em committed 4 years ago

c794c5c8

feat(data/dfinsupp): add submodule.bsupr_eq_range_dfinsupp_lsum (#9202)

eric-wieser committed 4 years ago

6f2d1ba2

kex-y committed 4 years ago

41b361f5

kex-y committed 4 years ago

589d7226

Merge branch 'JasonKYi/integrable_with_density' of https://github.com/leanprover-community/mathlib into JasonKYi/lintegral_with_density_eq

kex-y committed 4 years ago

c22d0e0d

Newer Older