root_X_pow_sub_C_pow — Mathlib

English

If n > 1 and a ∈ K, the root of X^n − C a in the adjoin-root construction is nonzero.

Русский

Если n > 1 и a ∈ K, корень из X^n − C a в конструкции adjoin-root ненулевой.

LaTeX

$$$(\text{AdjoinRoot.root}(X^n - C a)) \neq 0$ for $n>1$.$$

Lean4

theorem root_X_pow_sub_C_pow (n : ℕ) (a : K) : (AdjoinRoot.root (X ^ n - C a)) ^ n = AdjoinRoot.of _ a := by
  rw [← sub_eq_zero, ← AdjoinRoot.eval₂_root, eval₂_sub, eval₂_C, eval₂_pow, eval₂_X]

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