natSepDegree_smul_nonzero — Mathlib

English

Multiplying a polynomial f by a nonzero scalar x from the left, i.e., x • f, does not change its separable degree.

Русский

Умножение на ненулевой скаляр слева, t.е. x • f, не меняет разделяемую степень.

LaTeX

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

Lean4

@[simp]
theorem natSepDegree_smul_nonzero {x : F} (hx : x ≠ 0) : (x • f).natSepDegree = f.natSepDegree := by
  classical simp only [natSepDegree_eq_of_isAlgClosed (AlgebraicClosure F), aroots_smul_nonzero _ hx]

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