commonDenomOfFinset — Mathlib

English

The common denominator for a Finset of elements is defined as commonDenom S f s id and is an element of S.

Русский

Общий знаменатель финитного множества элементов определяется как commonDenom S f s id и является элементом S.

LaTeX

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

Lean4

/-- A choice of a common multiple of the denominators of a finite set of fractions. -/
noncomputable def commonDenomOfFinset (s : Finset M') : S :=
  commonDenom S f s id

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