natSepDegree_C_mul_X_sub_C_pow — Mathlib

English

If x ≠ 0, then the separable degree of C x · (X − C y)^n equals that of (X − C y)^n, i.e., 0 if n = 0, else 1.

Русский

Если x ≠ 0, то natSepDegree(C x · (X − C y)^n) = natSepDegree((X − C y)^n) = 0 при n=0, иначе 1.

LaTeX

$$$ (C x \cdot (X - C y)^n).\operatorname{natSepDegree} = \begin{cases} 0, & n=0 \\\ 1, & n>0 \end{cases}$$$

Lean4

theorem natSepDegree_C_mul_X_sub_C_pow {x y : F} {n : ℕ} (hx : x ≠ 0) :
    (C x * (X - C y) ^ n).natSepDegree = if n = 0 then 0 else 1 := by
  simp only [natSepDegree_C_mul _ hx, natSepDegree_X_sub_C_pow]

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