finsetIntegerMultiple — Mathlib

English

The finset of numerators after clearing denominators for a finite set s is obtained by applying integerMultiple to each element of the attached Finset.

Русский

Множество числителей после устранения знаменателей для конечного набора s получается применением integerMultiple к каждому элементу присоединённого Finset.

LaTeX

$$$\text{finsetIntegerMultiple }(M,s) = s.attach.image(\\text{integerMultiple}(M,s,\\mathrm{id}))$$$

Lean4

/-- The finset of numerators after clearing the denominators of a finite set of fractions. -/
noncomputable def finsetIntegerMultiple [DecidableEq R] (s : Finset S) : Finset R :=
  s.attach.image fun t => integerMultiple M s id t

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