ℚ as a normed group

instance Rat.instNormedAddCommGroup : NormedAddCommGroup ℚ

Equations

• Rat.instNormedAddCommGroup = NormedAddCommGroup.mk Rat.instNormedAddCommGroup.proof_1

@[simp]

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

@[simp]

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