abs_coe

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#NNRat.abs_coe

English

For q ∈ ℚ≥0, the absolute value of its rational embedding equals q: |q| = q.

Русский

Для q ∈ ℚ≥0 модуль числа, как элемента ℚ, равен самому q: |q| = q.

LaTeX

$$$|q| = q\quad( q \in \mathbb{Q}_{\ge 0}).$$$

Lean4

@[simp]
theorem abs_coe (q : ℚ≥0) : |(q : ℚ)| = q :=
  abs_of_nonneg
    q.2
      -- See note [specialised high priority simp lemma]

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

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

Разделы

Аффилиация

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