eq_degree — Mathlib

English

In exponential characteristic one, the separable degree equals the degree, i.e., hf.degree = f.natDegree.

Русский

При экспоненциальной характеристике, равной 1, разделимая степень равна степени: hf.degree = f.natDegree.

LaTeX

$$$\\text{If } \\mathrm{ExpChar}(F)=1,\\; hf.degree = f.natDegree$$$

Lean4

/-- In exponential characteristic one, the separable degree equals the degree. -/
theorem eq_degree {f : F[X]} (hf : HasSeparableContraction 1 f) : hf.degree = f.natDegree :=
  by
  let ⟨a, ha⟩ := hf.dvd_degree'
  rw [← ha, one_pow a, mul_one]

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