roots_C_mul_X_sub_C — Mathlib

English

For a ≠ 0, the linear polynomial C(a) X − C(b) has a unique root given by 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_sub_C (b : R) (ha : a ≠ 0) : (C a * X - C b).roots = {a⁻¹ * b} := by
  simp [roots_C_mul_X_sub_C_of_IsUnit b ⟨a, a⁻¹, mul_inv_cancel₀ ha, inv_mul_cancel₀ ha⟩]

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