commonDenom — Mathlib

English

The commonDenom function assigns to any finite family a single element of S that serves as a common denominator.

Русский

Функция commonDenom сопоставляет любой конечной семье единый элемент S, служащий общим знаменателем.

LaTeX

$$$\operatorname{commonDenom}(S,f)(s) \in S$$$

Lean4

/-- A choice of a common multiple of the denominators of a `Finset`-indexed family of fractions. -/
noncomputable def commonDenom {ι : Type*} (s : Finset ι) (g : ι → M') : S :=
  (exist_integer_multiples S f s g).choose

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