coe_nnabs

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#Rat.coe_nnabs

English

Coercing nnabs(x) back to ℚ yields |x|: (nnabs x) casts to ℚ equals |x|.

Русский

Отображение обратно в ℚ даёт |x|: (nnabs x)↑ = |x|.

LaTeX

$$ (\operatorname{nnabs}(x) : \mathbb{Q}) = |x| $$

Lean4

@[norm_cast, simp]
theorem coe_nnabs (x : ℚ) : (Rat.nnabs x : ℚ) = abs x :=
  rfl

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

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

Разделы

Аффилиация

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