root_X_sub_C — Mathlib

English

For any a in a ring, IsRoot (X − C a) b holds exactly when a = b; i.e., the linear polynomial X − C a has root b iff a = b.

Русский

Для любого a в кольце IsRoot (X − C a) b выполняется тогда и только тогда, когда a = b; т.е. линейный полином X − C a имеет корень b тогда и только тогда, когда a = b.

LaTeX

$$IsRoot( X - C a ) b ↔ a = b$$

Lean4

theorem root_X_sub_C : IsRoot (X - C a) b ↔ a = b := by rw [IsRoot.def, eval_sub, eval_X, eval_C, sub_eq_zero, eq_comm]

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