mathlib3
feat(analysis/normed_space): norms on ℤ and ℚ
#1570

Merged

feat(analysis/normed_space): norms on ℤ and ℚ #1570

mergify merged 4 commits into master from int-rat-normed

feat(analysis/normed_space): norms on ℤ and ℚ

ac858ce8

Add some `elim_cast` lemmas

bc7b533b

robertylewis commented on 2019-10-21

Add `@[simp]`, thanks @robertylewis

d5aafdc1

robertylewis approved these changes on 2019-10-23

robertylewis added ready-to-merge

Merge branch 'master' into int-rat-normed

567017d2

mergify merged 079e6ec9 into master 7 years ago

mergify deleted the int-rat-normed branch 7 years ago

Reviewers

robertylewis

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone