isMonicOfDegree_add_add_two — Mathlib

English

A polynomial is monic of degree 2 iff it can be written as X^2 + C a X + C b for some a,b ∈ R.

Русский

Полином мономичен степени 2 тогда, когда его можно записать как X^2 + C a X + C b.

LaTeX

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

Lean4

theorem isMonicOfDegree_add_add_two (a b : R) : IsMonicOfDegree (X ^ 2 + C a * X + C b) 2 :=
  by
  rw [add_assoc]
  exact
    (isMonicOfDegree_X_pow R 2).add_right <|
      calc
        _ ≤ max (C a * X).natDegree (C b).natDegree := natDegree_add_le ..
        _ = (C a * X).natDegree := by simp
        _ < 2 := natDegree_C_mul_le .. |>.trans natDegree_X_le |>.trans_lt one_lt_two

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