root_X_pow_sub_C_eq_zero_iff — Mathlib

English

Equivalence between root nonzero and a ≠ 0 holds: root ≠ 0 iff a ≠ 0.

Русский

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

LaTeX

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

Lean4

theorem root_X_pow_sub_C_eq_zero_iff {n : ℕ} {a : K} (H : Irreducible (X ^ n - C a)) :
    (AdjoinRoot.root (X ^ n - C a)) = 0 ↔ a = 0 :=
  by
  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  refine ⟨not_imp_not.mp (root_X_pow_sub_C_ne_zero' hn), ?_⟩
  rintro rfl
  have := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) rfl
  rw [this, pow_one, map_zero, sub_zero, ← mk_X, mk_self]

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