exists_integral_multiples — Mathlib

English

For any finite set s ⊂ A, there exists y ≠ 0 in R such that for all z ∈ s, y z is integral over R.

Русский

Для любого конечного множества s ⊂ A существует y ≠ 0 в R такое, что для каждого z ∈ s, y z интегрально над R.

LaTeX

$$$\forall s:\ Finset\ A,\ Exists\ y\neq 0,\ \forall z\in s,\ IsIntegral\ R\ (y\cdot z)$$$

Lean4

theorem _root_.Algebra.IsAlgebraic.exists_integral_multiples [NoZeroDivisors R] [alg : Algebra.IsAlgebraic R A]
    (s : Finset A) : ∃ y ≠ (0 : R), ∀ z ∈ s, IsIntegral R (y • z) :=
  by
  have := Algebra.IsAlgebraic.nontrivial R A
  choose r hr int using fun x ↦ (alg.1 x).exists_integral_multiple
  refine ⟨∏ x ∈ s, r x, Finset.prod_ne_zero_iff.mpr fun _ _ ↦ hr _, fun _ h ↦ ?_⟩
  classical rw [← Finset.prod_erase_mul _ _ h, mul_smul]
  exact (int _).smul _

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