exist_integer_multiples_of_finset

English

Let M be as above and s a finite set of fractions in S. Then there exists b ∈ M such that every a ∈ s is cleared to an integer by multiplying by b, i.e., IsInteger R ((b : R) • a) for all a ∈ s.

Русский

Пусть M и S как выше, тогда для конечного множества дробей s в S существует b ∈ M, так что каждый элемент s приводится к целому числу при умножении на b.

LaTeX

$$$\exists b \in M, \forall a \in s, \ IsInteger_R( (b : R) \cdot a )$$$

Lean4

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

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