num — Mathlib

English

Define num A x to be the numerator of x in its reduced fraction representation.

Русский

Определим num A x как числитель дроби x в представлении в виде несократимой дроби.

LaTeX

$$$\\mathrm{num}_A(x) := \\text{the numerator in the reduced fraction for }x$$$

Lean4

/-- `f.num x` is the numerator of `x : f.codomain` as a reduced fraction. -/
noncomputable def num (x : K) : A :=
  Classical.choose (exists_reduced_fraction A x)

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