mathlib3
chore(analysis): put lemmas in normed_field namespace
#1517

Merged

chore(analysis): put lemmas in normed_field namespace #1517

mergify merged 3 commits into master from normed_field_ns

chore(analysis): put lemmas in normed_field namespace

16b0c5ec

PatrickMassot requested a review from

sgouezel 6 years ago

PatrickMassot requested a review from

rwbarton 6 years ago

sgouezel approved these changes on 2019-10-08

sgouezel added ready-to-merge

Merge branch 'master' into normed_field_ns

975ccdd9

Merge branch 'master' into normed_field_ns

f3c45289

mergify merged 6b15eb29 into master 6 years ago

mergify deleted the normed_field_ns branch 6 years ago

Reviewers

sgouezel

rwbarton

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone