exist_integer_multiples_of_finset

English

Given a finite index set, there exists an S-multiple b such that each element g i becomes integer after multiplying by b.

Русский

Для конечного индекса существует S-умножитель b, такой что каждое g i становится целым после умножения на b.

LaTeX

$$$\exists b \in S, \forall i,\ IsInteger f (b \cdot g(i))$$$

Lean4

/-- We can clear the denominators of a finite set of fractions. -/
theorem exist_integer_multiples_of_finset (s : Finset M') : ∃ b : S, ∀ a ∈ s, IsInteger f ((b : R) • a) :=
  exist_integer_multiples S f s id

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