real_eq_abs

Mathlib.NumberTheory.Ostrowski

URI: https://scilib.ai/kg/mathlib#Rat.AbsoluteValue.real_eq_abs

English

The real absolute value on rationals coincides with the standard absolute value on rationals.

Русский

Действительное абсолютное значение на рациональных совпадает с стандартным абсолютным значением.

LaTeX

$$real r = |r| for r ∈ ℚ$$

Lean4

@[simp]
theorem real_eq_abs (r : ℚ) : real r = |r| :=
  (cast_abs r).symm

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru