isMonicOfDegree_two_iff — Mathlib

English

IsMonicOfDegree f 2 holds iff there exist a,b ∈ R such that f = X^2 + C a X + C b.

Русский

IsMonicOfDegree f 2 эквивалентно существованию a,b ∈ R с f = X^2 + C a X + C b.

LaTeX

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

Lean4

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_add_add_two a b⟩
  refine ⟨f.coeff 1, f.coeff 0, ext fun n ↦ ?_⟩
  rcases lt_trichotomy n 1 with hn | rfl | hn
  · obtain rfl : n = 0 := Nat.lt_one_iff.mp hn
    simp
  · simp
  · exact H.coeff_eq (isMonicOfDegree_add_add_two ..) (by cutsat)

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