mathlib3
feat(algebra/pointwise): More lemmas on pointwise multiplication
#997

Merged

feat(algebra/pointwise): More lemmas on pointwise multiplication #997

mergify merged 5 commits into master from pointwise-more

jcommelin requested a review 6 years ago

feat(algebra/pointwise): More lemmas on pointwise multiplication

74f9d615

Fix build, hopefully

7806fcad

Fix build

bfc26db6

sgouezel commented on 2019-05-08

to_additive + fix formatting

e9962131

Merge branch 'master' into pointwise-more

ce68fcc8

sgouezel approved these changes on 2019-05-09

sgouezel added ready-to-merge

mergify merged 5329bf3a into master 6 years ago

mergify deleted the pointwise-more branch 6 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone