den — Mathlib

English

Define den A x to be the denominator of x in its reduced fraction representation.

Русский

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

LaTeX

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

Lean4

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

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