leanprover-community/mathlib

Pull Requests Commits

refactored proof

erdOne committed 4 years ago

82471214

refactored stuff

erdOne committed 4 years ago

0297771f

refactored stuff

erdOne committed 4 years ago

93402492

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

erdOne committed 4 years ago

fbbe8ade

proved stacks#00XK

erdOne committed 4 years ago

b539b7c2

feat(analysis/calculus/fderiv): generalize `const_smul` lemmas (#9399)

urkud committed 4 years ago

5dfb76f5

feat(data/nat/choose/cast): Cast of binomial coefficients equals a Pochhammer polynomial (#9394)

YaelDillies committed 4 years ago

954896a1

refactor(data/fin): drop `fin.cast_add_right` (#9371)

urkud committed 4 years ago

9a30f8cf

chore(order/*): rename `strict_mono_{incr,decr}_on` to `strict_{mono,anti}_on` (#9401)

eric-wieser committed 4 years ago

850784cf

chore(order): globally replace "antimono" with "antitone" (#9400)

eric-wieser committed 4 years ago

14727997

docs(docker): adjust readme to reflect that the PR was merged (#9303)

eric-wieser committed 4 years ago

d1c68ef7

chore(measure_theory/decomposition/lebesgue): rename `radon_nikodym_deriv` to `rn_deriv` (#9386)

kex-y committed 4 years ago

cafd6fbc

refactor(analysis/special_functions/trigonometric): split file (#9340)

kim-em committed 4 years ago

a4b92a3f

refactor(measure_theory/measure/hausdorff): move `dimH` to a new file, redefine (#9391)

urkud committed 4 years ago

62abfe52

feat(algebra/pointwise): add smul_set_inter (#9374)

alexjbest committed 4 years ago

432271f9

feat(topology/sheaves/stalks): Generalize from Type to algebraic categories (#9357)

justus-springer committed 4 years ago

996783ce

feat(algebra/module/pointwise_pi): add a file with lemmas on smul_pi (#9369)

alexjbest committed 4 years ago

865ad478

docs(undergrad): Add trigonometric Weierstrass (#9393)

PatrickMassot committed 4 years ago

b3ca07f8

feat(field_theory/is_alg_closed): more isomorphisms of algebraic closures (#9376)

ChrisHughes24 committed 4 years ago

4ae46db4

refactor(linear_algebra/charpoly): move linear_algebra/charpoly to linear_algebra/matrix/charpoly (#9368)

riccardobrasca committed 4 years ago

453f2183

refactor(data/fin,*): redefine `insert_nth`, add lemmas (#9349)

urkud committed 4 years ago

a2517af6

feat(algebra/order/ring): add odd_neg, odd_abs, generalize dvd/abs lemmas (#9362)

Ruben-VandeVelde committed 4 years ago

83470aff

refactor(analysis/convex/function): generalize definition of `convex_on`/`concave_on` to allow any (ordered) scalars (#9389)

YaelDillies committed 4 years ago

def1c02a

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

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

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

Older