mathlib

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

feat(analysis/normed_space): norms on ℤ and ℚ (#1570) * feat(analysis/normed_space): norms on ℤ and ℚ * Add some `elim_cast` lemmas * Add `@[simp]`, thanks @robertylewis Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>