mathlib documentation

topology.instances.rat

Topology on the ratonal numbers #

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

@[protected, instance]
noncomputable def rat.metric_space  :
Equations
theorem rat.dist_eq (x y : ) :
@[simp, norm_cast]
theorem rat.dist_cast (x y : ) :
@[simp, norm_cast]
@[simp, norm_cast]
@[protected, instance]
@[protected, instance]
@[protected, instance]
theorem rat.continuous_mul  :
continuous (λ (p : × ), p.fst * p.snd)
@[protected, instance]