separable_X_pow_sub_C_of_irreducible

English

If X^n − C a is irreducible over K and certain primitive roots exist, then it is separable.

Русский

Если X^n − C a ирредуцируем над K и существует подходящий примитивный корень, то многочлен separable.

LaTeX

$$(X^n - C a).Separable$$

Lean4

/-- Also see `Polynomial.separable_X_pow_sub_C_unit` -/
theorem separable_X_pow_sub_C_of_irreducible : (X ^ n - C a).Separable :=
  by
  letI := Fact.mk H
  letI : Algebra K K[n√a] := inferInstance
  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  by_cases hn' : n = 1
  · rw [hn', pow_one]; exact separable_X_sub_C
  have ⟨ζ, hζ⟩ := hζ
  rw [mem_primitiveRoots (Nat.pos_of_ne_zero <| ne_zero_of_irreducible_X_pow_sub_C H)] at hζ
  rw [← separable_map (algebraMap K K[n√a]), Polynomial.map_sub, Polynomial.map_pow, map_C, map_X,
    AdjoinRoot.algebraMap_eq,
    X_pow_sub_C_eq_prod (hζ.map_of_injective (algebraMap K _).injective) hn (root_X_pow_sub_C_pow n a),
    separable_prod_X_sub_C_iff']
  exact
    (hζ.map_of_injective (algebraMap K K[n√a]).injective).injOn_pow_mul
      (root_X_pow_sub_C_ne_zero (lt_of_le_of_ne (show 1 ≤ n from hn) (Ne.symm hn')) _)

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