English
Let L be a finite extension of the fraction field of A, and S a finite set of elements of L. There exists a nonzero a in A such that each x in S becomes integral after multiplication by a, i.e., a·x is integral over A.
Русский
Пусть L — конечное расширение дробей A, и S — конечное множество элементов L. Существует не нулевой элемент a в A, такой что для каждого x в S произведение a·x интегрировано над A.
LaTeX
$$$$\\exists\, y \\neq 0 \\in A\\;\\forall\, x \\in s,\\; \\text{IsIntegral}_A(y\\cdot x)$$$$
Lean4
/-- Send a set of `x`s in a finite extension `L` of the fraction field of `R`
to `(y : R) • x ∈ integralClosure R L`. -/
theorem exists_integral_multiples (s : Finset L) : ∃ y ≠ (0 : A), ∀ x ∈ s, IsIntegral A (y • x) :=
have := IsLocalization.isAlgebraic K (nonZeroDivisors A)
have := Algebra.IsAlgebraic.trans A K L
Algebra.IsAlgebraic.exists_integral_multiples ..
