ℚ as a normed group

instance Rat.instNormedAddCommGroup : NormedAddCommGroup ℚ

Equations

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

@[simp]

theorem Rat.norm_cast_real (r : ℚ) : ‖↑r‖ = ‖r‖

@[simp]

theorem Int.norm_cast_rat (m : ℤ) : ‖↑m‖ = ‖m‖