galois_poly_separable — Mathlib

English

Let K be a commutative ring and p a prime with p | q, and suppose Char_p(K) = p. Then the polynomial X^q - X ∈ K[X] is separable.

Русский

Пусть K — кольцо коммутативное, p — простое число, п divides q и характеристика K равна p. Тогда многочлен X^q - X ∈ K[X] разделим.

LaTeX

$$Separable(X^{q} - X) (in K[X] under Char_p K = p and p ∣ q)$$

Lean4

theorem galois_poly_separable {K : Type*} [CommRing K] (p q : ℕ) [CharP K p] (h : p ∣ q) :
    Separable (X ^ q - X : K[X]) := by
  use 1, X ^ q - X - 1
  rw [← CharP.cast_eq_zero_iff K[X] p] at h
  rw [derivative_sub, derivative_X_pow, derivative_X, C_eq_natCast, h]
  ring

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