English
An element is algebraic over A iff it is algebraic over the field of fractions of A, under suitable tower conditions.
Русский
Элемент алгебраичен над A тогда и только тогда, когда он алгебраичен над полем дробей A при подходящих условиях модуля шкалы.
LaTeX
$$$\text{IsAlgebraic}_A(x) \iff \text{IsAlgebraic}_K(x)$ under the scalar tower$$
Lean4
theorem integerNormalization_eq_zero_iff {p : K[X]} : integerNormalization (nonZeroDivisors A) p = 0 ↔ p = 0 :=
by
refine Polynomial.ext_iff.trans (Polynomial.ext_iff.trans ?_).symm
obtain ⟨⟨b, nonzero⟩, hb⟩ := integerNormalization_spec (nonZeroDivisors A) p
constructor <;> intro h i
· rw [coeff_zero, ← to_map_eq_zero_iff (K := K), hb i, h i, coeff_zero, smul_zero]
· have hi := h i
rw [Polynomial.coeff_zero, ← @to_map_eq_zero_iff A _ K, hb i, Algebra.smul_def] at hi
apply Or.resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero hi)
intro h
apply mem_nonZeroDivisors_iff_ne_zero.mp nonzero
exact to_map_eq_zero_iff.mp h
