natAbs_num_coe — Mathlib

English

Let q be a nonnegative rational number. Then the numerator of q, viewed as a rational, has natural absolute value equal to q.num; since q.num is a natural, natAbs(q.num) = q.num.

Русский

Пусть q ∈ ℚ≥0. Тогда числитель q, рассматриваемый как рациональное число, удовлетворяет |q.num| = q.num; то есть q.num.natAbs = q.num.

LaTeX

$$$ (q : \mathbb{Q}).num.natAbs = q.num $$$

Lean4

theorem natAbs_num_coe : (q : ℚ).num.natAbs = q.num :=
  rfl

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