Mathlib.Analysis.Normed.Group.Rat

Rat.instNormedAddCommGroup instance

: NormedAddCommGroup ℚ

Full source

instance instNormedAddCommGroup : NormedAddCommGroup ℚ where
  norm r := ‖(r : ℝ)‖
  dist_eq r₁ r₂ := by simp only [Rat.dist_eq, norm, Rat.cast_sub]

The Normed Additive Commutative Group Structure on Rational Numbers

Informal description

The rational numbers $\mathbb{Q}$ form a normed additive commutative group, where the norm of a rational number $x$ is given by its absolute value $\|x\| = |x|$, and the metric structure is induced by the norm.

Rat.norm_cast_real theorem

(r : ℚ) : ‖(r : ℝ)‖ = ‖r‖

Full source

@[norm_cast, simp 1001]
-- Porting note: increase priority to prevent the left-hand side from simplifying
theorem norm_cast_real (r : ℚ) : ‖(r : ℝ)‖ = ‖r‖ :=
  rfl

Norm Preservation of Rational Numbers in Real Embedding

Informal description

For any rational number $r$, the norm of its canonical embedding into the real numbers equals the norm of $r$ in $\mathbb{Q}$, i.e., $\|(r : \mathbb{R})\| = \|r\|$.

Int.norm_cast_rat theorem

(m : ℤ) : ‖(m : ℚ)‖ = ‖m‖

Full source

@[norm_cast, simp]
theorem _root_.Int.norm_cast_rat (m : ℤ) : ‖(m : ℚ)‖ = ‖m‖ := by
  rw [← Rat.norm_cast_real, ← Int.norm_cast_real]; congr 1

Norm Preservation of Integers in Rational Embedding: $\|(m : \mathbb{Q})\| = \|m\|$

Informal description

For any integer $m$, the norm of its canonical embedding into the rational numbers equals the norm of $m$ in $\mathbb{Z}$, i.e., $\|(m : \mathbb{Q})\| = \|m\|$.