operator_norm): replace subspace with …
#955

Merged

refactor(analysis/normed_space/operator_norm): replace subspace with … #955

mergify merged 4 commits into leanprover-community:master from sgouezel:operator_norm2

refactor(analysis/normed_space/operator_norm): replace subspace with …

65caac81

sgouezel requested a review 6 years ago

digama0 dismissed these changes on 2019-04-21

refactor(analysis/normed_space/operator_norm): add coercions

be3348d2

mergify dismissed their stale review 6 years ago

Pull request has been modified.

Merge branch 'master' into operator_norm2

7be12bcc

avigad approved these changes on 2019-04-25

avigad added ready-to-merge

Merge branch 'master' into 'operator_norm2'

76cc387a

mergify merged 038f809c into master 6 years ago

sgouezel deleted the operator_norm2 branch 6 years ago

Reviewers

avigad

digama0

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone