X_pow_sub_C_irreducible_iff_of_prime

English

For prime p, irreducible X^p − C a iff ∀ b, b^p ≠ a (same as X_pow_sub_C_irreducible_iff_of_prime).

Русский

Для простого p ирр X^p − C a тогда и только тогда, когда нет b, такого что b^p = a.

LaTeX

$$$\text{Irreducible}(X^p - C a) \iff \forall b, b^p \neq a$$$

Lean4

theorem X_pow_sub_C_irreducible_iff_of_prime {p : ℕ} (hp : p.Prime) {a : K} :
    Irreducible (X ^ p - C a) ↔ ∀ b, b ^ p ≠ a :=
  ⟨(pow_ne_of_irreducible_X_pow_sub_C · dvd_rfl hp.ne_one), X_pow_sub_C_irreducible_of_prime hp⟩

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