isMonicOfDegree_sub_add_two — Mathlib

English

The quadratic polynomial X^2 − a X + b is monic of degree 2 for any a,b in R.

Русский

Квадратичный многочлен X^2 − a X + b моноичен степени 2 для любых a,b в R.

LaTeX

$$$\\operatorname{IsMonicOfDegree}\\bigl(X^2 - C a \\cdot X + C b, 2\\bigr)$$$

Lean4

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

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