coeff_zero_mem_comap_of_root_mem_of_eval_mem

English

If a ∈ I, then a + b ∈ I iff b ∈ I.

Русский

Если a ∈ I, то a + b ∈ I тогда и только тогда, когда b ∈ I.

LaTeX

$$$\forall I\; (a,b:\alpha),\; a \in I \rightarrow (a+b \in I \iff b \in I).$$$

Lean4

theorem coeff_zero_mem_comap_of_root_mem_of_eval_mem {r : S} (hr : r ∈ I) {p : R[X]} (hp : p.eval₂ f r ∈ I) :
    p.coeff 0 ∈ I.comap f :=
  by
  rw [← p.divX_mul_X_add, eval₂_add, eval₂_C, eval₂_mul, eval₂_X] at hp
  refine mem_comap.mpr ((I.add_mem_iff_right ?_).mp hp)
  exact I.mul_mem_left _ hr

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