exists_nonzero_dvd — Mathlib

English

Same as above: there exists a nonzero r with s dividing the image of r.

Русский

То же самое: существует ненулевой элемент r, такой что изображение r делится на s.

LaTeX

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

Lean4

theorem exists_nonzero_dvd {s : S} (hRs : IsAlgebraic R s) (hs : s ∈ S⁰) : ∃ r : R, r ≠ 0 ∧ s ∣ algebraMap R S r :=
  by
  obtain ⟨q, hq0, hq⟩ := hRs.exists_nonzero_coeff_and_aeval_eq_zero hs
  have key := map_dvd (aeval s) (X_dvd_sub_C (p := q))
  rw [map_sub, hq, zero_sub, dvd_neg, aeval_X, aeval_C] at key
  exact ⟨q.coeff 0, hq0, key⟩

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