roots_degree_eq_one — Mathlib

English

If a polynomial p has degree 1, then its roots are exactly the single element given by −(p.coeff 1)⁻¹ p.coeff 0.

Русский

Если полином p имеет степень 1, то его корни соответствуют единственному элементу −(p.coeff 1)⁻¹ p.coeff 0.

LaTeX

$$$ \deg p = 1 \Rightarrow p.roots = \{ -((p.coeff 1)^{-1} \cdot p.coeff 0) \}$$$

Lean4

theorem roots_degree_eq_one (h : degree p = 1) : p.roots = {-((p.coeff 1)⁻¹ * p.coeff 0)} :=
  by
  rw [eq_X_add_C_of_degree_le_one (show degree p ≤ 1 by rw [h])]
  have : p.coeff 1 ≠ 0 := coeff_ne_zero_of_eq_degree h
  simp [roots_C_mul_X_add_C _ this]

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