mathlib3
feat(*): more `prod`-related (continuous) linear maps and their derivatives
#2277

Merged

feat(*): more `prod`-related (continuous) linear maps and their derivatives #2277

mergify merged 3 commits into master from prod-map

feat(*): more `prod`-related (continuous) linear maps and their deriv…

d0501017

sgouezel commented on 2020-03-29

sgouezel added awaiting-author

Make `R` argument of `continuous_linear_equiv.refl` explicit

4b1908d8

urkud removed awaiting-author

urkud added awaiting-review

sgouezel approved these changes on 2020-03-30

sgouezel removed awaiting-review

sgouezel added ready-to-merge

Merge remote-tracking branch 'community/master' into prod-map

ce7ba546

mergify merged c5181d11 into master 6 years ago

urkud deleted the prod-map branch 6 years ago

Reviewers

sgouezel

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone