mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero

English

A polynomial P lies in the span of {C(X - Ca), X - Cb} if and only if (P.eval b).eval a = 0.

Русский

Полином P принадлежит к порожденному подпространству от {C(X - Ca), X - Cb} тогда и только тогда, когда (P.eval b).eval a = 0.

LaTeX

$$$P \in \operatorname{Ideal}.\operatorname{span} \{C(X - C a), X - C b\} \iff (P.eval b).eval a = 0$$$

Lean4

theorem mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero {b : R[X]} {P : R[X][X]} :
    P ∈ Ideal.span {C (X - C a), X - C b} ↔ (P.eval b).eval a = 0 :=
  by
  rw [Ideal.mem_span_pair]
  constructor <;> intro h
  · rcases h with ⟨_, _, rfl⟩
    simp only [eval_C, eval_X, eval_add, eval_sub, eval_mul, add_zero, mul_zero, sub_self]
  · rcases dvd_iff_isRoot.mpr h with ⟨p, hp⟩
    rcases @X_sub_C_dvd_sub_C_eval _ b _ P with ⟨q, hq⟩
    exact ⟨C p, q, by rw [mul_comm, mul_comm q, eq_add_of_sub_eq' hq, hp, C_mul]⟩

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