Documentation

Mathlib.Topology.Instances.Rat

Topology on the rational numbers #

The structure of a metric space on is introduced in this file, induced from .

theorem Rat.dist_eq (x : ) (y : ) :
dist x y = |x - y|
@[simp]
theorem Rat.dist_cast (x : ) (y : ) :
dist x y = dist x y
@[simp]
theorem Nat.dist_cast_rat (x : ) (y : ) :
dist x y = dist x y
@[simp]
theorem Int.dist_cast_rat (x : ) (y : ) :
dist x y = dist x y