roots_C_mul_X_add_C — Mathlib

English

For a ≠ 0, the linear polynomial C(a) X + C(b) has a unique root at −a⁻¹ b in the target ring S.

Русский

Для a ≠ 0 линейный полином C(a) X + C(b) имеет единственный корень −a⁻¹ b в кольце S.

LaTeX

$$$ (C a \cdot X + C b).roots = \{ -(a^{-1} \cdot b) \} \quad \text{for } a \neq 0 $$$

Lean4

theorem roots_C_mul_X_add_C (b : R) (ha : a ≠ 0) : (C a * X + C b).roots = {-(a⁻¹ * b)} := by
  simp [roots_C_mul_X_add_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

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