exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem

English

From (a − b) ∈ I and (c − d) ∈ I it follows that ac − bd ∈ I (I is two-sided).

Русский

Из того, что a−b ∈ I и c−d ∈ I следует ac−bd ∈ I (I — двусторонний идеал).

LaTeX

$$$\forall I\; (I: \text{Ideal } \alpha)\; [I.IsTwoSided] \; (a-b)\in I \rightarrow (c-d)\in I \rightarrow (a c - b d) \in I.$$$

Lean4

theorem exists_coeff_ne_zero_mem_comap_of_non_zero_divisor_root_mem {r : S}
    (r_non_zero_divisor : ∀ {x}, x * r = 0 → x = 0) (hr : r ∈ I) {p : R[X]} :
    p ≠ 0 → p.eval₂ f r = 0 → ∃ i, p.coeff i ≠ 0 ∧ p.coeff i ∈ I.comap f :=
  by
  refine p.recOnHorner ?_ ?_ ?_
  · intro h
    contradiction
  · intro p a coeff_eq_zero a_ne_zero _ _ hp
    refine ⟨0, ?_, coeff_zero_mem_comap_of_root_mem hr hp⟩
    simp [coeff_eq_zero, a_ne_zero]
  · intro p p_nonzero ih _ hp
    rw [eval₂_mul, eval₂_X] at hp
    obtain ⟨i, hi, mem⟩ := ih p_nonzero (r_non_zero_divisor hp)
    refine ⟨i + 1, ?_, ?_⟩
    · simp [hi]
    · simpa [hi] using mem

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