degree_X_pow_add_C — Mathlib

English

For any nontrivial R and a ∈ R, deg((X^n) + C a) equals n, provided n > 0.

Русский

Пусть R не тривиально. Для любого a ∈ R, deg(X^n + C a) = n, если n > 0.

LaTeX

$$$\deg((X)^n + C a) = n$$$

Lean4

theorem degree_X_pow_add_C {n : ℕ} (hn : 0 < n) (a : R) : degree ((X : R[X]) ^ n + C a) = n :=
  by
  have : degree (C a) < degree ((X : R[X]) ^ n) := degree_C_le.trans_lt <| by rwa [degree_X_pow, Nat.cast_pos]
  rw [degree_add_eq_left_of_degree_lt this, degree_X_pow]

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