natSepDegree_eq_one_iff_of_monic — Mathlib

English

For f,g, either (f=0 ∧ g=0) or IsCoprime f g implies equality (f*g).natSepDegree = f.natSepDegree + g.natSepDegree.

Русский

Для f,g: либо (f=0 ∧ g=0), либо IsCoprime f g, тогда выполняется (f*g).natSepDegree = f.natSepDegree + g.natSepDegree.

LaTeX

$$$ (f \cdot g).natSepDegree = f.natSepDegree + g.natSepDegree \iff (f = 0 \wedge g = 0) \lor IsCoprime f g $$$

Lean4

/-- A monic irreducible polynomial over a field `F` of exponential characteristic `q` has
separable degree one if and only if it is of the form `X ^ (q ^ n) - C y`
for some `n : ℕ` and `y : F`. -/
theorem natSepDegree_eq_one_iff_of_monic (q : ℕ) [ExpChar F q] (hm : f.Monic) (hi : Irreducible f) :
    f.natSepDegree = 1 ↔ ∃ (n : ℕ) (y : F), f = X ^ q ^ n - C y := by
  simp_rw [hi.natSepDegree_eq_one_iff_of_monic' q hm, map_sub, expand_X, expand_C]

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