isMonicOfDegree_two_iff' — Mathlib

English

IsMonicOfDegree f 2 is equivalent to f = X^2 − C a · X + C b for some a,b in R.

Русский

IsMonicOfDegree f 2 эквивалентно f = X^2 − C a · X + C b для некоторых a,b ∈ R.

LaTeX

$$$IsMonicOfDegree(f, 2) \\iff \\exists a,b\\in R,\\ f = X^2 - C a \\cdot X + C b$$$

Lean4

/-- A version of `Polynomial.isMonicOfDegree_two_iff` with negated middle coefficient. -/
theorem isMonicOfDegree_two_iff' {f : R[X]} : IsMonicOfDegree f 2 ↔ ∃ a b : R, f = X ^ 2 - C a * X + C b :=
  by
  refine ⟨fun H ↦ ?_, fun ⟨a, b, h⟩ ↦ h ▸ isMonicOfDegree_sub_add_two a b⟩
  simp only [sub_eq_add_neg, ← neg_mul, ← map_neg]
  obtain ⟨a, b, h⟩ := isMonicOfDegree_two_iff.mp H
  exact ⟨-a, b, (neg_neg a).symm ▸ h⟩

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