Documentation

Mathlib.Analysis.Normed.Group.Rat

ℚ as a normed group #

source
🔸 coverage
instance Rat.instNormedAddCommGroup :
NormedAddCommGroup ℚ
Equations
    source
    📐 coverage
    @[simp]
    theorem Rat.norm_cast_real (r : ℚ) :
    ‖↑r‖ = ‖r‖
    source
    📐 coverage
    @[simp]
    theorem Int.norm_cast_rat (m : ℤ) :
    ‖↑m‖ = ‖m‖