num — Mathlib

English

The numerator of a RatFunc is defined as the first component of the pair numDenom(x).

Русский

Числитель рациональной функции определён как первая координата пары numDenom(x).

LaTeX

$$$\operatorname{num}(x) = \operatorname{fst}(\operatorname{numDenom}(x))$$$

Lean4

/-- `RatFunc.num` is the numerator of a rational function,
normalized such that the denominator is monic. -/
def num (x : RatFunc K) : K[X] :=
  x.numDenom.1

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