# ℚ as a normed group #

source
instance Rat.instNormedAddCommGroup :
NormedAddCommGroup ℚ
Equations

- Rat.instNormedAddCommGroup = { norm := fun (r : ℚ) => ‖↑r‖, toAddCommGroup := Rat.addCommGroup, toMetricSpace := Rat.instMetricSpace, dist_eq := Rat.instNormedAddCommGroup._proof_1 }

source
@[simp]
theorem Rat.norm_cast_real (r : ℚ) :
‖↑r‖ = ‖r‖
source
@[simp]
theorem Int.norm_cast_rat (m : ℤ) :
‖↑m‖ = ‖m‖