root_X_pow_sub_C_ne_zero_iff

Mathlib.FieldTheory.KummerPolynomial

URI: https://scilib.ai/kg/mathlib#root_X_pow_sub_C_ne_zero_iff

← MathLib Explorer

English

Equivalence: root is nonzero iff a ≠ 0 (re-statement of irreducibility consequences).

Русский

Эквивалентность: корень ненулевой тогда и только тогда, когда a ≠ 0.

LaTeX

$$$(\text{root}) \neq 0 \iff a \neq 0$$$

Lean4

theorem root_X_pow_sub_C_ne_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
    (AdjoinRoot.root (X ^ n - C a)) ≠ 0 ↔ a ≠ 0 :=
  (root_X_pow_sub_C_eq_zero_iff H).not

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru