num_coe — Mathlib

English

For q ∈ ℚ≥0, the numerator of the underlying rational equals the numerator of q: (q : ℚ).num = q.num.

Русский

Для q ∈ ℚ≥0 числитель рационального числа после приведения равен числу q.num.

LaTeX

$$$\bigl( q : \mathbb{Q} \bigr).\text{num} = q.\text{num} \quad (q \in \mathbb{Q}_{\ge 0}).$$$

Lean4

@[norm_cast]
theorem num_coe (q : ℚ≥0) : (q : ℚ).num = q.num := by
  simp only [num, Int.natCast_natAbs, Rat.num_nonneg, coe_nonneg, abs_of_nonneg]

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