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

Merged

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

mergify merged 8 commits into master from scale-set-lem

feat(algebra/pointwise): more lemmas about scaling sets

35344033

fix(analysis/convex): refactor proofs for `scale_set`

d6bacd2c

Merge branch 'master' of https://github.com/leanprover-community/math…

cf6b2af5

cipher1024 assigned

sgouezel 6 years ago

jcommelin commented on 2020-01-29

robertylewis added awaiting-review

jlpaca force pushed from 01fc275f to 2fc00ccb 6 years ago

jlpaca force pushed from 2fc00ccb to bd03b897 6 years ago

feat(algebra/pointwise): re-organise file

bd03b897

fix(algebra/pointwise): resolve conflicts with analysis/convex

32dba011

feat(algebra/pointwise): remove `pointwise_mul_action`

51c33558

Merge branch 'master' of https://github.com/leanprover-community/math…

d342bc7a

sgouezel removed awaiting-review

sgouezel added ready-to-merge

sgouezel approved these changes on 2020-02-02

Merge branch 'master' into scale-set-lem

029163de

mergify merged 1843bfc9 into master 6 years ago

mergify deleted the scale-set-lem branch 6 years ago

Reviewers

sgouezel

jcommelin

Assignees

sgouezel

Labels

ready-to-merge

Milestone

No milestone