natSepDegree_C_mul — Mathlib

English

Multiplying a polynomial f by a nonzero field element x via a constant C x does not change its separable degree.

Русский

Умножение многочлена f на ненулевой элемент поля через константное умножение C x не изменяет его разделяемую степень.

LaTeX

$$$ (C\!x \cdot f).\operatorname{natSepDegree} = f.\operatorname{natSepDegree}$$$

Lean4

@[simp]
theorem natSepDegree_C_mul {x : F} (hx : x ≠ 0) : (C x * f).natSepDegree = f.natSepDegree := by
  classical simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_C_mul _ hx]

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