root_X_pow_sub_C_ne_zero — Mathlib

English

The root of X^n − C a is zero if and only if a = 0.

Русский

Корень из X^n − C a равен нулю тогда и только тогда, когда a = 0.

LaTeX

$$$\text{root}(X^n - C a) = 0 \iff a = 0$$$

Lean4

theorem root_X_pow_sub_C_ne_zero {n : ℕ} (hn : 1 < n) (a : K) : (AdjoinRoot.root (X ^ n - C a)) ≠ 0 :=
  mk_ne_zero_of_natDegree_lt (monic_X_pow_sub_C _ (Nat.ne_zero_of_lt hn)) X_ne_zero <| by
    rwa [natDegree_X_pow_sub_C, natDegree_X]

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