exists_nonzero_eq_adjoin_mul — Mathlib

English

If s is algebraic over R and s is a nonzerodivisor in S, there exists r ≠ 0 in R such that s divides algebraMap_R^S(r).

Русский

Если s алгебраичен над R и не ноль-делитель в S, существует r ≠ 0 в R such that s | algebraMap_R^S(r).

LaTeX

$$$\exists r:\ R, r \neq 0 \land s \mid \operatorname{algebraMap}_R^S(r)$$$

Lean4

theorem exists_nonzero_eq_adjoin_mul {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ S⁰) :
    ∃ᵉ (t ∈ Algebra.adjoin R { s }) (r ≠ (0 : R)), s * t = algebraMap R S r :=
  by
  have ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs
  have ⟨p, hp⟩ := X_dvd_sub_C (p := q)
  refine ⟨aeval s p, aeval_mem_adjoin_singleton _ _, _, neg_ne_zero.mpr hq0, ?_⟩
  apply_fun aeval s at hp
  rwa [map_sub, hq, zero_sub, map_mul, aeval_X, aeval_C, ← map_neg, eq_comm] at hp

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