ℚ as a normed group

@[instance_reducible]

instance Rat.instNormedAddCommGroup : NormedAddCommGroup ℚ

Equations

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

@[simp]

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

@[simp]

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