operator_norm): cleanup
#1906

Merged

doc (analysis/normed_space/operator_norm): cleanup #1906

mergify merged 3 commits into leanprover-community:master from sgouezel:op_norm_doc

doc (analysis/normed_space/operator_norm): cleanup

bbd4e6a1

typo

f77306c8

jcommelin approved these changes on 2020-01-25

jcommelin added ready-to-merge

Merge branch 'master' into op_norm_doc

a2fd09c7

mergify merged 70772422 into master 6 years ago

sgouezel deleted the op_norm_doc branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone