natSepDegree_eq — Mathlib

English

If n ≠ 0, then (f^n).natSepDegree = f.natSepDegree.

Русский

Если n ≠ 0, то (f^n).natSepDegree = f.natSepDegree.

LaTeX

$$$ n \neq 0 \Rightarrow (f^n).natSepDegree = f.natSepDegree $$$

Lean4

/-- If `g` is a separable contraction of `f`, then the separable degree of `f` is equal to
the degree of `g`. -/
theorem natSepDegree_eq {g : Polynomial F} {q : ℕ} [ExpChar F q] (h : IsSeparableContraction q f g) :
    f.natSepDegree = g.natDegree := by
  obtain ⟨h1, m, h2⟩ := h
  rw [← h2, natSepDegree_expand, h1.natSepDegree_eq_natDegree]

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