mathlib documentation

Topology on the integers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

@[protected, instance]
theorem int.dist_eq (x y : ) :
@[simp, norm_cast]
theorem int.pairwise_one_le_dist  :
pairwise (λ (m n : ), 1 has_dist.dist m n)
theorem int.ball_eq_Ioo (x : ) (r : ) :
@[protected, instance]