English
Let R,S,A be as specified with NoZeroDivisors R and algebraic over R. For any finite set s ⊂ A, there exists y ≠ 0 in R such that y z is integral over R for all z ∈ s.
Русский
Пусть R,S,A удовлетворяют условиям, NoZeroDivisors(R) и алгебраически над R. Для любого конечного множества s ⊂ A существует y ≠ 0 в R, такое что y z интеграл над R для всех z ∈ s.
LaTeX
$$[NoZeroDivisors R] ∧ [alg : Algebra.IsAlgebraic R A] ⟹ ∀ (s : Finset A), ∃ y ≠ (0 : R), ∀ z ∈ s, IsIntegral R (y • z)$$
Lean4
theorem exists_integral_multiple (hz : IsAlgebraic R z) : ∃ y ≠ (0 : R), IsIntegral R (y • z) :=
by
by_cases inj : Function.Injective (algebraMap R A); swap
· rw [injective_iff_map_eq_zero] at inj; push_neg at inj
have ⟨r, eq, ne⟩ := inj
exact ⟨r, ne, by simpa [← algebraMap_smul A, eq, zero_smul] using isIntegral_zero⟩
have ⟨p, p_ne_zero, px⟩ := hz
set a := p.leadingCoeff
have a_ne_zero : a ≠ 0 := mt Polynomial.leadingCoeff_eq_zero.mp p_ne_zero
have x_integral : IsIntegral R (algebraMap R A a * z) :=
⟨p.integralNormalization, monic_integralNormalization p_ne_zero,
integralNormalization_aeval_eq_zero px fun _ ↦ (map_eq_zero_iff _ inj).mp⟩
exact ⟨_, a_ne_zero, Algebra.smul_def a z ▸ x_integral⟩
