Topology on the ratonal numbers #
The structure of a metric space on ℚ
is introduced in this file, induced from ℝ
.
@[protected, instance]
Equations
- rat.metric_space = metric_space.induced coe rat.metric_space._proof_1 real.metric_space
@[simp, norm_cast]
@[simp, norm_cast]