English
A real-valued absolute value on a ring endows the ring with a NormedRing structure, where the norm is the absolute value, and the distance is given by the absolute value of the difference.
Русский
Реальная абсолютная величина на кольце определяет структуру NormedRing: нормa задаётся как абсолютная величина, а расстояние как абсолютная величина разности.
LaTeX
$$$\\|x\\| = v(x),\\quad d(x,y) = v(x-y)\\text{ for a real absolute value }v\\text{ on }R$, giving a NormedRing structure on $R$.$$
Lean4
/-- A real absolute value on a ring determines a `NormedRing` structure. -/
noncomputable def toNormedRing {R : Type*} [Ring R] (v : AbsoluteValue R ℝ) : NormedRing R
where
norm := v
dist x y := v (x - y)
dist_eq _ _ := rfl
dist_self x := by simp only [sub_self, map_zero]
dist_comm := v.map_sub
dist_triangle := v.sub_le
edist_dist x y := rfl
norm_mul_le x y := (v.map_mul x y).le
eq_of_dist_eq_zero := by simp only [AbsoluteValue.map_sub_eq_zero_iff, imp_self, implies_true]
