Theorems · Theorem · field theory

Polynomial.unique_separable_of_irreducible

∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F},
  Irreducible f →
    0 < p →
      ∀ (n₁ : ℕ) (g₁ : Polynomial F),
        g₁.Separable →
          (Polynomial.expand F (p ^ n₁)) g₁ = f →
            ∀ (n₂ : ℕ) (g₂ : Polynomial F), g₂.Separable → (Polynomial.expand F (p ^ n₂)) g₂ = f → n₁ = n₂ ∧ g₁ = g₂

Defined in

Mathlib.FieldTheory.Separable

Cited by

0 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldCharP