separable_C_mul_X_pow_add_C_mul_X_add_C'

English

If R has characteristic p and p divides n, and b is a unit, then a X^n + b X + c is separable.

Русский

Если характеристика R равна p и p делит n, а b — единица, то a X^n + b X + c сепарабелен.

LaTeX

$$$ \operatorname{Separable}\left( C a \cdot X^n + C b \cdot X + C c \right)$ under char p and p | n$$

Lean4

/-- If `R` is of characteristic `p`, `p ∣ n` and `b` is a unit,
then `a * X ^ n + b * X + c` is separable. -/
theorem separable_C_mul_X_pow_add_C_mul_X_add_C' (p n : ℕ) (a b c : R) [CharP R p] (hn : p ∣ n) (hb : IsUnit b) :
    (C a * X ^ n + C b * X + C c).Separable :=
  separable_C_mul_X_pow_add_C_mul_X_add_C a b c ((CharP.cast_eq_zero_iff R p n).2 hn) hb

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