root_X_pow_sub_C_ne_zero' — Mathlib

English

If n ≠ 1, then a ≠ 0 whenever X^n − C a is irreducible.

Русский

Если n ≠ 1, то при иррeдубрируемости X^n − C a следует a ≠ 0.

LaTeX

$$$n \neq 1 \Rightarrow (a \neq 0).$$$

Lean4

theorem root_X_pow_sub_C_ne_zero' {n : ℕ} {a : K} (hn : 0 < n) (ha : a ≠ 0) : (AdjoinRoot.root (X ^ n - C a)) ≠ 0 :=
  by
  obtain (rfl | hn) := (Nat.succ_le_iff.mpr hn).eq_or_lt
  · rw [pow_one]
    intro e
    refine mk_ne_zero_of_natDegree_lt (monic_X_sub_C a) (C_ne_zero.mpr ha) (by simp) ?_
    trans AdjoinRoot.mk (X - C a) (X - (X - C a))
    · rw [sub_sub_cancel]
    · rw [map_sub, mk_self, sub_zero, mk_X, e]
  · exact root_X_pow_sub_C_ne_zero hn a

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