exists_nonzero_coeff_and_aeval_eq_zero

English

If s is algebraic over R, and s is a nonzerodivisor in S, then there exists t in Adjoin_R({s}) and r ≠ 0 with s t = algebraMap_R^S(r).

Русский

Если s алгебраичен над R и неократим в S, то существует t ∈ Adjoin_R({s}) и r ≠ 0 такая что s t = algebraMap_R^S(r).

LaTeX

$$$\exists t \in \mathrm{Algebra.adjoin}\ R\{s\} , \exists r \neq 0,\ s t = \operatorname{algebraMap}_R^S(r)$$$

Lean4

theorem exists_nonzero_coeff_and_aeval_eq_zero {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ S⁰) :
    ∃ q : R[X], q.coeff 0 ≠ 0 ∧ aeval s q = 0 :=
  by
  obtain ⟨p, hp0, hp⟩ := hRs
  obtain ⟨q, hpq, hq⟩ := exists_eq_pow_rootMultiplicity_mul_and_not_dvd p hp0 0
  simp only [C_0, sub_zero, X_pow_mul, X_dvd_iff] at hpq hq
  rw [hpq, map_mul, aeval_X_pow] at hp
  exact ⟨q, hq, (S⁰.pow_mem hs (rootMultiplicity 0 p)).2 (aeval s q) hp⟩

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