doc-next-gen

Mathlib.FieldTheory.Separable

Module docstring

{"# Separable polynomials

We define a polynomial to be separable if it is coprime with its derivative. We prove basic properties about separable polynomials here.

Main definitions

  • Polynomial.Separable f: a polynomial f is separable iff it is coprime with its derivative.
  • IsSeparable K x: an element x is separable over K iff the minimal polynomial of x over K is separable.
  • Algebra.IsSeparable K L: L is separable over K iff every element in L is separable over K.

"}

Polynomial.Separable definition
(f : R[X]) : Prop
Full source 
/-- A polynomial is separable iff it is coprime with its derivative. -/
@[stacks 09H1 "first part"]
def Separable (f : R[X]) : Prop :=
  IsCoprime f (derivative f)
Separable polynomial
Informal description
A polynomial \( f \) over a ring \( R \) is called *separable* if it is coprime with its derivative \( f' \), meaning there exist polynomials \( a \) and \( b \) in \( R[X] \) such that \( a \cdot f + b \cdot f' = 1 \).
Polynomial.separable_def theorem
(f : R[X]) : f.Separable ↔ IsCoprime f (derivative f)
Full source 
theorem separable_def (f : R[X]) : f.Separable ↔ IsCoprime f (derivative f) :=
  Iff.rfl
Characterization of Separable Polynomials via Coprimality with Derivative
Informal description
A polynomial $f$ over a ring $R$ is separable if and only if $f$ and its derivative $f'$ are coprime.
Polynomial.separable_def' theorem
(f : R[X]) : f.Separable ↔ ∃ a b : R[X], a * f + b * (derivative f) = 1
Full source 
theorem separable_def' (f : R[X]) : f.Separable ↔ ∃ a b : R[X], a * f + b * (derivative f) = 1 :=
  Iff.rfl
Characterization of Separable Polynomials via Bézout's Identity
Informal description
A polynomial $f$ over a ring $R$ is separable if and only if there exist polynomials $a, b \in R[X]$ such that $a \cdot f + b \cdot f' = 1$, where $f'$ denotes the derivative of $f$.
Polynomial.Separable.ne_zero theorem
[Nontrivial R] {f : R[X]} (h : f.Separable) : f ≠ 0
Full source 
theorem Separable.ne_zero [Nontrivial R] {f : R[X]} (h : f.Separable) : f ≠ 0 :=
  (not_separable_zero <| · ▸ h)
Nonzero Condition for Separable Polynomials over Nontrivial Rings
Informal description
Let $R$ be a nontrivial ring and $f \in R[X]$ be a polynomial. If $f$ is separable, then $f$ is not the zero polynomial.
Polynomial.separable_one theorem
: (1 : R[X]).Separable
Full source 
@[simp]
theorem separable_one : (1 : R[X]).Separable :=
  isCoprime_one_left
Separability of the Constant Polynomial 1
Informal description
The constant polynomial $1$ over any ring $R$ is separable, i.e., it is coprime with its derivative.
Polynomial.separable_of_subsingleton theorem
[Subsingleton R] (f : R[X]) : f.Separable
Full source 
@[nontriviality]
theorem separable_of_subsingleton [Subsingleton R] (f : R[X]) : f.Separable := by
  simp [Separable, IsCoprime, eq_iff_true_of_subsingleton]
Separability of Polynomials over Subsingleton Rings
Informal description
For any polynomial $f$ over a ring $R$ that is a subsingleton (i.e., has at most one element), $f$ is separable.
Polynomial.Separable.of_mul_left theorem
{f g : R[X]} (h : (f * g).Separable) : f.Separable
Full source 
theorem Separable.of_mul_left {f g : R[X]} (h : (f * g).Separable) : f.Separable := by
  have := h.of_mul_left_left; rw [derivative_mul] at this
  exact IsCoprime.of_mul_right_left (IsCoprime.of_add_mul_left_right this)
Left Factor of Separable Product is Separable
Informal description
For any polynomials $f$ and $g$ over a ring $R$, if the product $f \cdot g$ is separable, then $f$ is separable.
Polynomial.Separable.of_mul_right theorem
{f g : R[X]} (h : (f * g).Separable) : g.Separable
Full source 
theorem Separable.of_mul_right {f g : R[X]} (h : (f * g).Separable) : g.Separable := by
  rw [mul_comm] at h
  exact h.of_mul_left
Right Factor of Separable Product is Separable
Informal description
For any polynomials $f$ and $g$ over a ring $R$, if the product $f \cdot g$ is separable, then $g$ is separable.
Polynomial.Separable.of_dvd theorem
{f g : R[X]} (hf : f.Separable) (hfg : g ∣ f) : g.Separable
Full source 
theorem Separable.of_dvd {f g : R[X]} (hf : f.Separable) (hfg : g ∣ f) : g.Separable := by
  rcases hfg with ⟨f', rfl⟩
  exact Separable.of_mul_left hf
Divisor of Separable Polynomial is Separable
Informal description
For any polynomials $f$ and $g$ over a ring $R$, if $f$ is separable and $g$ divides $f$, then $g$ is separable.
Polynomial.separable_gcd_left theorem
{F : Type*} [Field F] [DecidableEq F[X]] {f : F[X]} (hf : f.Separable) (g : F[X]) : (EuclideanDomain.gcd f g).Separable
Full source 
theorem separable_gcd_left {F : Type*} [Field F] [DecidableEq F[X]]
    {f : F[X]} (hf : f.Separable) (g : F[X]) :
    (EuclideanDomain.gcd f g).Separable :=
  Separable.of_dvd hf (EuclideanDomain.gcd_dvd_left f g)
Separability of GCD with a Separable Polynomial
Informal description
Let $F$ be a field and $f, g \in F[X]$ be polynomials. If $f$ is separable, then the greatest common divisor $\gcd(f, g)$ is also separable.
Polynomial.separable_gcd_right theorem
{F : Type*} [Field F] [DecidableEq F[X]] {g : F[X]} (f : F[X]) (hg : g.Separable) : (EuclideanDomain.gcd f g).Separable
Full source 
theorem separable_gcd_right {F : Type*} [Field F] [DecidableEq F[X]]
    {g : F[X]} (f : F[X]) (hg : g.Separable) :
    (EuclideanDomain.gcd f g).Separable :=
  Separable.of_dvd hg (EuclideanDomain.gcd_dvd_right f g)
Separability of GCD with a Separable Polynomial
Informal description
Let $F$ be a field and $f, g$ be polynomials over $F$. If $g$ is separable, then the greatest common divisor $\gcd(f, g)$ is also separable.
Polynomial.Separable.isCoprime theorem
{f g : R[X]} (h : (f * g).Separable) : IsCoprime f g
Full source 
theorem Separable.isCoprime {f g : R[X]} (h : (f * g).Separable) : IsCoprime f g := by
  have := h.of_mul_left_left; rw [derivative_mul] at this
  exact IsCoprime.of_mul_right_right (IsCoprime.of_add_mul_left_right this)
Separability of Product Implies Coprimality of Factors
Informal description
For any two polynomials $f$ and $g$ over a ring $R$, if the product $f \cdot g$ is separable, then $f$ and $g$ are coprime.
Polynomial.Separable.of_pow' theorem
{f : R[X]} : ∀ {n : ℕ} (_h : (f ^ n).Separable), IsUnit f ∨ f.Separable ∧ n = 1 ∨ n = 0
Full source 
theorem Separable.of_pow' {f : R[X]} :
    ∀ {n : ℕ} (_h : (f ^ n).Separable), IsUnitIsUnit f ∨ f.Separable ∧ n = 1 ∨ n = 0
  | 0 => fun _h => Or.inr <| Or.inr rfl
  | 1 => fun h => Or.inr <| Or.inl ⟨pow_one f ▸ h, rfl⟩
  | n + 2 => fun h => by
    rw [pow_succ, pow_succ] at h
    exact Or.inl (isCoprime_self.1 h.isCoprime.of_mul_left_right)
Separability of Powers: $f^n$ separable implies $f$ unit or ($f$ separable and $n=1$) or $n=0$
Informal description
Let $f$ be a polynomial over a ring $R$ and let $n$ be a natural number. If the power $f^n$ is separable, then either: 1. $f$ is a unit in $R[X]$, or 2. $f$ is separable and $n = 1$, or 3. $n = 0$.
Polynomial.Separable.of_pow theorem
{f : R[X]} (hf : ¬IsUnit f) {n : ℕ} (hn : n ≠ 0) (hfs : (f ^ n).Separable) : f.Separable ∧ n = 1
Full source 
theorem Separable.of_pow {f : R[X]} (hf : ¬IsUnit f) {n : ℕ} (hn : n ≠ 0)
    (hfs : (f ^ n).Separable) : f.Separable ∧ n = 1 :=
  (hfs.of_pow'.resolve_left hf).resolve_right hn
Separability of Powers: Non-unit Case ($f^n$ separable implies $f$ separable and $n=1$)
Informal description
Let $f$ be a non-unit polynomial over a ring $R$ and let $n$ be a non-zero natural number. If the power $f^n$ is separable, then $f$ is separable and $n = 1$.
Polynomial.Separable.map theorem
{p : R[X]} (h : p.Separable) {f : R →+* S} : (p.map f).Separable
Full source 
theorem Separable.map {p : R[X]} (h : p.Separable) {f : R →+* S} : (p.map f).Separable :=
  let ⟨a, b, H⟩ := h
  ⟨a.map f, b.map f, by
    rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
      Polynomial.map_one]⟩
Separability is preserved under polynomial mapping
Informal description
Let $p$ be a separable polynomial over a ring $R$, and let $f \colon R \to S$ be a ring homomorphism. Then the polynomial $p$ mapped via $f$ (denoted $p \circ f$) is also separable over $S$.
Associated.separable theorem
{f g : R[X]} (ha : Associated f g) (h : f.Separable) : g.Separable
Full source 
theorem _root_.Associated.separable {f g : R[X]}
    (ha : Associated f g) (h : f.Separable) : g.Separable := by
  obtain ⟨⟨u, v, h1, h2⟩, ha⟩ := ha
  obtain ⟨a, b, h⟩ := h
  refine ⟨a * v + b * derivative v, b * v, ?_⟩
  replace h := congr($h * $(h1))
  have h3 := congr(derivative $(h1))
  simp only [← ha, derivative_mul, derivative_one] at h3 ⊢
  calc
    _ = (a * f + b * derivative f) * (u * v)
      + (b * f) * (derivative u * v + u * derivative v) := by ring1
    _ = 1 := by rw [h, h3]; ring1
Separability of Associated Polynomials
Informal description
Let $f$ and $g$ be polynomials over a ring $R$ such that $f$ and $g$ are associated (i.e., there exists a unit $u$ such that $f = u \cdot g$). If $f$ is separable, then $g$ is also separable.
Associated.separable_iff theorem
{f g : R[X]} (ha : Associated f g) : f.Separable ↔ g.Separable
Full source 
theorem _root_.Associated.separable_iff {f g : R[X]}
    (ha : Associated f g) : f.Separable ↔ g.Separable := ⟨ha.separable, ha.symm.separable⟩
Separability Equivalence for Associated Polynomials
Informal description
Let $f$ and $g$ be polynomials over a ring $R$ such that $f$ and $g$ are associated (i.e., there exists a unit $u$ such that $f = u \cdot g$). Then $f$ is separable if and only if $g$ is separable.
Polynomial.Separable.mul_unit theorem
{f g : R[X]} (hf : f.Separable) (hg : IsUnit g) : (f * g).Separable
Full source 
theorem Separable.mul_unit {f g : R[X]} (hf : f.Separable) (hg : IsUnit g) : (f * g).Separable :=
  (associated_mul_unit_right f g hg).separable hf
Separability of Product with Unit Polynomial
Informal description
Let $f$ and $g$ be polynomials over a ring $R$. If $f$ is separable and $g$ is a unit (i.e., invertible), then the product polynomial $f \cdot g$ is separable.
Polynomial.Separable.unit_mul theorem
{f g : R[X]} (hf : IsUnit f) (hg : g.Separable) : (f * g).Separable
Full source 
theorem Separable.unit_mul {f g : R[X]} (hf : IsUnit f) (hg : g.Separable) : (f * g).Separable :=
  (associated_unit_mul_right g f hf).separable hg
Separability of Unit Multiplied by Separable Polynomial
Informal description
Let $f$ and $g$ be polynomials over a ring $R$. If $f$ is a unit in $R[X]$ and $g$ is separable, then the product polynomial $f \cdot g$ is also separable.
Polynomial.Separable.eval₂_derivative_ne_zero theorem
[Nontrivial S] (f : R →+* S) {p : R[X]} (h : p.Separable) {x : S} (hx : p.eval₂ f x = 0) : (derivative p).eval₂ f x ≠ 0
Full source 
theorem Separable.eval₂_derivative_ne_zero [Nontrivial S] (f : R →+* S) {p : R[X]}
    (h : p.Separable) {x : S} (hx : p.eval₂ f x = 0) :
    (derivative p).eval₂ f x ≠ 0 := by
  intro hx'
  obtain ⟨a, b, e⟩ := h
  apply_fun Polynomial.eval₂ f x at e
  simp only [eval₂_add, eval₂_mul, hx, mul_zero, hx', add_zero, eval₂_one, zero_ne_one] at e
Nonvanishing of Derivative at Roots of Separable Polynomials
Informal description
Let \( R \) and \( S \) be rings with \( S \) nontrivial, and let \( f : R \to S \) be a ring homomorphism. For any separable polynomial \( p \in R[X] \) and any element \( x \in S \) such that \( p \) evaluated at \( x \) via \( f \) is zero (i.e., \( \text{eval}_2(f, p, x) = 0 \)), the derivative of \( p \) evaluated at \( x \) via \( f \) is nonzero (i.e., \( \text{eval}_2(f, p', x) \neq 0 \)).
Polynomial.Separable.aeval_derivative_ne_zero theorem
[Nontrivial S] [Algebra R S] {p : R[X]} (h : p.Separable) {x : S} (hx : aeval x p = 0) : aeval x (derivative p) ≠ 0
Full source 
theorem Separable.aeval_derivative_ne_zero [Nontrivial S] [Algebra R S] {p : R[X]}
    (h : p.Separable) {x : S} (hx : aeval x p = 0) :
    aevalaeval x (derivative p) ≠ 0 :=
  h.eval₂_derivative_ne_zero (algebraMap R S) hx
Nonvanishing of Derivative at Roots of Separable Polynomials in Algebra Evaluation
Informal description
Let $R$ and $S$ be rings with $S$ nontrivial, and let $S$ be an $R$-algebra. For any separable polynomial $p \in R[X]$ and any element $x \in S$ such that the evaluation of $p$ at $x$ via the algebra map is zero (i.e., $\text{aeval}_x p = 0$), the evaluation of the derivative $p'$ at $x$ via the algebra map is nonzero (i.e., $\text{aeval}_x p' \neq 0$).
Polynomial.isUnit_of_self_mul_dvd_separable theorem
{p q : R[X]} (hp : p.Separable) (hq : q * q ∣ p) : IsUnit q
Full source 
theorem isUnit_of_self_mul_dvd_separable {p q : R[X]} (hp : p.Separable) (hq : q * q ∣ p) :
    IsUnit q := by
  obtain ⟨p, rfl⟩ := hq
  apply isCoprime_self.mp
  have : IsCoprime (q * (q * p))
      (q * (derivative q * p + derivative q * p + q * derivative p)) := by
    simp only [← mul_assoc, mul_add]
    dsimp only [Separable] at hp
    convert hp using 1
    rw [derivative_mul, derivative_mul]
    ring
  exact IsCoprime.of_mul_right_left (IsCoprime.of_mul_left_left this)
Square factor of separable polynomial implies unit
Informal description
Let $p$ and $q$ be polynomials over a ring $R$. If $p$ is separable and $q^2$ divides $p$, then $q$ is a unit in $R[X]$.
Polynomial.emultiplicity_le_one_of_separable theorem
{p q : R[X]} (hq : ¬IsUnit q) (hsep : Separable p) : emultiplicity q p ≤ 1
Full source 
theorem emultiplicity_le_one_of_separable {p q : R[X]} (hq : ¬IsUnit q) (hsep : Separable p) :
    emultiplicity q p ≤ 1 := by
  contrapose! hq
  apply isUnit_of_self_mul_dvd_separable hsep
  rw [← sq]
  apply pow_dvd_of_le_emultiplicity
  exact Order.add_one_le_of_lt hq
Extended multiplicity bound for separable polynomials: $\text{emultiplicity}\, q\, p \leq 1$ when $p$ is separable and $q$ is not a unit
Informal description
For any polynomials $p$ and $q$ over a ring $R$, if $q$ is not a unit and $p$ is separable, then the extended multiplicity of $q$ in $p$ is at most 1. In other words, $q$ can divide $p$ at most once (i.e., $q$ is not a repeated factor of $p$).
Polynomial.Separable.squarefree theorem
{p : R[X]} (hsep : Separable p) : Squarefree p
Full source 
/-- A separable polynomial is square-free.

See `PerfectField.separable_iff_squarefree` for the converse when the coefficients are a perfect
field. -/
theorem Separable.squarefree {p : R[X]} (hsep : Separable p) : Squarefree p := by
  classical
  rw [squarefree_iff_emultiplicity_le_one p]
  exact fun f => or_iff_not_imp_right.mpr fun hunit => emultiplicity_le_one_of_separable hunit hsep
Separable polynomials are squarefree
Informal description
For any polynomial $p$ over a ring $R$, if $p$ is separable, then $p$ is squarefree (i.e., $p$ has no repeated irreducible factors).
Polynomial.separable_X_sub_C theorem
{x : R} : Separable (X - C x)
Full source 
theorem separable_X_sub_C {x : R} : Separable (X - C x) := by
  simpa only [sub_eq_add_neg, C_neg] using separable_X_add_C (-x)
Separability of Linear Polynomial $X - x$
Informal description
For any element $x$ in a ring $R$, the polynomial $X - x$ is separable, i.e., it is coprime with its derivative.
Polynomial.Separable.mul theorem
{f g : R[X]} (hf : f.Separable) (hg : g.Separable) (h : IsCoprime f g) : (f * g).Separable
Full source 
theorem Separable.mul {f g : R[X]} (hf : f.Separable) (hg : g.Separable) (h : IsCoprime f g) :
    (f * g).Separable := by
  rw [separable_def, derivative_mul]
  exact
    ((hf.mul_right h).add_mul_left_right _).mul_left ((h.symm.mul_right hg).mul_add_right_right _)
Product of Separable Coprime Polynomials is Separable
Informal description
Let $f$ and $g$ be polynomials over a ring $R$. If $f$ is separable, $g$ is separable, and $f$ and $g$ are coprime, then their product $f \cdot g$ is also separable.
Polynomial.separable_prod' theorem
{ι : Sort _} {f : ι → R[X]} {s : Finset ι} : (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable
Full source 
theorem separable_prod' {ι : Sort _} {f : ι → R[X]} {s : Finset ι} :
    (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) →
      (∀ x ∈ s, (f x).Separable) → (∏ x ∈ s, f x).Separable := by
  classical
  exact Finset.induction_on s (fun _ _ => separable_one) fun a s has ih h1 h2 => by
    simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2; rw [prod_insert has]
    exact
      h2.1.mul (ih h1.2.2 h2.2)
        (IsCoprime.prod_right fun i his => h1.1.2 i his <| Ne.symm <| ne_of_mem_of_not_mem his has)
Separability of Finite Product of Pairwise Coprime Separable Polynomials
Informal description
Let $R$ be a ring, $\iota$ a type, $f \colon \iota \to R[X]$ a family of polynomials, and $s$ a finite subset of $\iota$. If for any distinct elements $x, y \in s$ the polynomials $f(x)$ and $f(y)$ are coprime, and each $f(x)$ is separable for $x \in s$, then the product $\prod_{x \in s} f(x)$ is separable.
Polynomial.separable_prod theorem
{ι : Sort _} [Fintype ι] {f : ι → R[X]} (h1 : Pairwise (IsCoprime on f)) (h2 : ∀ x, (f x).Separable) : (∏ x, f x).Separable
Full source 
theorem separable_prod {ι : Sort _} [Fintype ι] {f : ι → R[X]} (h1 : Pairwise (IsCoprimeIsCoprime on f))
    (h2 : ∀ x, (f x).Separable) : (∏ x, f x).Separable :=
  separable_prod' (fun _x _hx _y _hy hxy => h1 hxy) fun x _hx => h2 x
Separability of Finite Product of Pairwise Coprime Separable Polynomials
Informal description
Let $R$ be a ring and $\iota$ a finite type. Given a family of polynomials $f \colon \iota \to R[X]$ such that: 1. The polynomials are pairwise coprime (i.e., $f(x)$ and $f(y)$ are coprime for any distinct $x, y \in \iota$), and 2. Each polynomial $f(x)$ is separable (i.e., coprime with its derivative), then the product $\prod_{x \in \iota} f(x)$ is separable.
Polynomial.Separable.inj_of_prod_X_sub_C theorem
[Nontrivial R] {ι : Sort _} {f : ι → R} {s : Finset ι} (hfs : (∏ i ∈ s, (X - C (f i))).Separable) {x y : ι} (hx : x ∈ s) (hy : y ∈ s) (hfxy : f x = f y) : x = y
Full source 
theorem Separable.inj_of_prod_X_sub_C [Nontrivial R] {ι : Sort _} {f : ι → R} {s : Finset ι}
    (hfs : (∏ i ∈ s, (X - C (f i))).Separable) {x y : ι} (hx : x ∈ s) (hy : y ∈ s)
    (hfxy : f x = f y) : x = y := by
  classical
  by_contra hxy
  rw [← insert_erase hx, prod_insert (not_mem_erase _ _), ←
    insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (not_mem_erase _ _), ←
    mul_assoc, hfxy, ← sq] at hfs
  cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2
Injectivity of Root Indices for Separable Product of Linear Factors
Informal description
Let $R$ be a nontrivial ring, $\iota$ a type, $f \colon \iota \to R$ a function, and $s$ a finite subset of $\iota$. If the product $\prod_{i \in s} (X - f(i))$ is a separable polynomial over $R$, then for any $x, y \in s$ with $f(x) = f(y)$, we have $x = y$.
Polynomial.Separable.injective_of_prod_X_sub_C theorem
[Nontrivial R] {ι : Sort _} [Fintype ι] {f : ι → R} (hfs : (∏ i, (X - C (f i))).Separable) : Function.Injective f
Full source 
theorem Separable.injective_of_prod_X_sub_C [Nontrivial R] {ι : Sort _} [Fintype ι] {f : ι → R}
    (hfs : (∏ i, (X - C (f i))).Separable) : Function.Injective f := fun _x _y hfxy =>
  hfs.inj_of_prod_X_sub_C (mem_univ _) (mem_univ _) hfxy
Injectivity of Root Indices for Separable Product of Linear Factors over Finite Type
Informal description
Let $R$ be a nontrivial ring and $\iota$ a finite type. Given a function $f \colon \iota \to R$ such that the polynomial $\prod_{i \in \iota} (X - f(i))$ is separable, then $f$ is injective.
Polynomial.nodup_of_separable_prod theorem
[Nontrivial R] {s : Multiset R} (hs : Separable (Multiset.map (fun a => X - C a) s).prod) : s.Nodup
Full source 
theorem nodup_of_separable_prod [Nontrivial R] {s : Multiset R}
    (hs : Separable (Multiset.map (fun a => X - C a) s).prod) : s.Nodup := by
  rw [Multiset.nodup_iff_ne_cons_cons]
  rintro a t rfl
  refine not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs ?_)
  simpa only [Multiset.map_cons, Multiset.prod_cons] using mul_dvd_mul_left _ (dvd_mul_right _ _)
Separability of product of linear factors implies distinctness of roots
Informal description
Let $R$ be a nontrivial ring and $s$ a multiset of elements in $R$. If the polynomial $\prod_{a \in s} (X - a)$ is separable, then the multiset $s$ has no duplicate elements (i.e., it is a set).
Polynomial.separable_X_pow_sub_C_unit theorem
{n : ℕ} (u : Rˣ) (hn : IsUnit (n : R)) : Separable (X ^ n - C (u : R))
Full source 
/-- If `IsUnit n` in a `CommRing R`, then `X ^ n - u` is separable for any unit `u`. -/
theorem separable_X_pow_sub_C_unit {n : ℕ} (u : Rˣ) (hn : IsUnit (n : R)) :
    Separable (X ^ n - C (u : R)) := by
  nontriviality R
  rcases n.eq_zero_or_pos with (rfl | hpos)
  · simp at hn
  apply (separable_def' (X ^ n - C (u : R))).2
  obtain ⟨n', hn'⟩ := hn.exists_left_inv
  refine ⟨-C ↑u⁻¹, C (↑u⁻¹ : R) * C n' * X, ?_⟩
  rw [derivative_sub, derivative_C, sub_zero, derivative_pow X n, derivative_X, mul_one]
  calc
    -C ↑u⁻¹ * (X ^ n - C ↑u) + C ↑u⁻¹ * C n' * X * (↑n * X ^ (n - 1)) =
        C (↑u⁻¹ * ↑u) - C ↑u⁻¹ * X ^ n + C ↑u⁻¹ * C (n' * ↑n) * (X * X ^ (n - 1)) := by
      simp only [C.map_mul, C_eq_natCast]
      ring
    _ = 1 := by
      simp only [Units.inv_mul, hn', C.map_one, mul_one, ← pow_succ',
        Nat.sub_add_cancel (show 1 ≤ n from hpos), sub_add_cancel]
Separability of $X^n - u$ when $n$ is a unit in $R$
Informal description
Let $R$ be a commutative ring, $n$ a natural number, and $u$ a unit in $R$. If the image of $n$ in $R$ is a unit, then the polynomial $X^n - u$ is separable (i.e., coprime with its derivative).
Polynomial.separable_C_mul_X_pow_add_C_mul_X_add_C theorem
{n : ℕ} (a b c : R) (hn : (n : R) = 0) (hb : IsUnit b) : (C a * X ^ n + C b * X + C c).Separable
Full source 
/-- If `n = 0` in `R` and `b` is a unit, then `a * X ^ n + b * X + c` is separable. -/
theorem separable_C_mul_X_pow_add_C_mul_X_add_C
    {n : ℕ} (a b c : R) (hn : (n : R) = 0) (hb : IsUnit b) :
    (C a * X ^ n + C b * X + C c).Separable := by
  set f := C a * X ^ n + C b * X + C c
  obtain ⟨e, hb⟩ := hb.exists_left_inv
  refine ⟨-derivative f, f + C e, ?_⟩
  have hderiv : derivative f = C b := by
    simp [hn, f, map_add derivative, derivative_C, derivative_X_pow]
  rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
Separability of $a X^n + b X + c$ when $n=0$ and $b$ is a unit
Informal description
Let $R$ be a ring, $n$ a natural number, and $a, b, c \in R$. If $n = 0$ in $R$ and $b$ is a unit in $R$, then the polynomial $a X^n + b X + c$ is separable (i.e., coprime with its derivative).
Polynomial.separable_C_mul_X_pow_add_C_mul_X_add_C' theorem
(p n : ℕ) (a b c : R) [CharP R p] (hn : p ∣ n) (hb : IsUnit b) : (C a * X ^ n + C b * X + C c).Separable
Full source 
/-- If `R` is of characteristic `p`, `p ∣ n` and `b` is a unit,
then `a * X ^ n + b * X + c` is separable. -/
theorem separable_C_mul_X_pow_add_C_mul_X_add_C'
    (p n : ℕ) (a b c : R) [CharP R p] (hn : p ∣ n) (hb : IsUnit b) :
    (C a * X ^ n + C b * X + C c).Separable :=
  separable_C_mul_X_pow_add_C_mul_X_add_C a b c ((CharP.cast_eq_zero_iff R p n).2 hn) hb
Separability of $a X^n + b X + c$ in characteristic $p$ when $p \mid n$ and $b$ is a unit
Informal description
Let $R$ be a ring of characteristic $p$, and let $a, b, c \in R$ with $b$ a unit. For any natural numbers $p$ and $n$ such that $p$ divides $n$, the polynomial $a X^n + b X + c$ is separable (i.e., coprime with its derivative).
Polynomial.rootMultiplicity_le_one_of_separable theorem
[Nontrivial R] {p : R[X]} (hsep : Separable p) (x : R) : rootMultiplicity x p ≤ 1
Full source 
theorem rootMultiplicity_le_one_of_separable [Nontrivial R] {p : R[X]} (hsep : Separable p)
    (x : R) : rootMultiplicity x p ≤ 1 := by
  classical
  by_cases hp : p = 0
  · simp [hp]
  rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞),
    Nat.cast_one, ← (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]
  apply emultiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep
Root Multiplicity Bound for Separable Polynomials: $\text{rootMultiplicity}\, x\, p \leq 1$
Informal description
For any nontrivial ring $R$ and separable polynomial $p \in R[X]$, the root multiplicity of any element $x \in R$ in $p$ is at most 1. In other words, if $p$ is separable, then no root of $p$ has multiplicity greater than 1.
Polynomial.count_roots_le_one theorem
[DecidableEq R] {p : R[X]} (hsep : Separable p) (x : R) : p.roots.count x ≤ 1
Full source 
theorem count_roots_le_one [DecidableEq R] {p : R[X]} (hsep : Separable p) (x : R) :
    p.roots.count x ≤ 1 := by
  rw [count_roots p]
  exact rootMultiplicity_le_one_of_separable hsep x
Root Multiplicity Bound for Separable Polynomials: $\text{count}\, x\, p.\text{roots} \leq 1$
Informal description
For any separable polynomial $p$ over a nontrivial ring $R$ with decidable equality, and for any element $x \in R$, the multiplicity of $x$ in the multiset of roots of $p$ is at most 1, i.e., $\text{count}\, x\, p.\text{roots} \leq 1$.
Polynomial.nodup_roots theorem
{p : R[X]} (hsep : Separable p) : p.roots.Nodup
Full source 
theorem nodup_roots {p : R[X]} (hsep : Separable p) : p.roots.Nodup := by
  classical
  exact Multiset.nodup_iff_count_le_one.mpr (count_roots_le_one hsep)
Distinct Roots of Separable Polynomials
Informal description
For any separable polynomial $p$ over a nontrivial ring $R$, the multiset of roots of $p$ has no duplicate elements, i.e., $\text{Nodup}(p.\text{roots})$.
Polynomial.separable_iff_derivative_ne_zero theorem
{f : F[X]} (hf : Irreducible f) : f.Separable ↔ derivative f ≠ 0
Full source 
theorem separable_iff_derivative_ne_zero {f : F[X]} (hf : Irreducible f) :
    f.Separable ↔ derivative f ≠ 0 :=
  ⟨fun h1 h2 => hf.not_isUnit <| isCoprime_zero_right.1 <| h2 ▸ h1, fun h =>
    EuclideanDomain.isCoprime_of_dvd (mt And.right h) fun g hg1 _hg2 ⟨p, hg3⟩ hg4 =>
      let ⟨u, hu⟩ := (hf.isUnit_or_isUnit hg3).resolve_left hg1
      have : f ∣ derivative f := by
        conv_lhs => rw [hg3, ← hu]
        rwa [Units.mul_right_dvd]
      not_lt_of_le (natDegree_le_of_dvd this h) <|
        natDegree_derivative_lt <| mt derivative_of_natDegree_zero h⟩
Separability Criterion for Irreducible Polynomials: $f$ separable $\iff$ $f' \neq 0$
Informal description
Let $F$ be a field and $f \in F[X]$ be an irreducible polynomial. Then $f$ is separable if and only if its derivative $f'$ is not the zero polynomial.
Polynomial.separable_map theorem
{S} [CommRing S] [Nontrivial S] (f : F →+* S) {p : F[X]} : (p.map f).Separable ↔ p.Separable
Full source 
theorem separable_map {S} [CommRing S] [Nontrivial S] (f : F →+* S) {p : F[X]} :
    (p.map f).Separable ↔ p.Separable := by
  refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
  obtain ⟨m, hm⟩ := Ideal.exists_maximal S
  have := Separable.map H (f := Ideal.Quotient.mk m)
  rwa [map_map, separable_def, derivative_map, isCoprime_map] at this
Separability is preserved under polynomial mapping if and only if the original polynomial is separable
Informal description
Let $F$ and $S$ be commutative rings with $S$ nontrivial, and let $f \colon F \to S$ be a ring homomorphism. For any polynomial $p \in F[X]$, the polynomial $p$ mapped via $f$ (denoted $p \circ f$) is separable over $S$ if and only if $p$ is separable over $F$.
Polynomial.separable_prod_X_sub_C_iff' theorem
{ι : Sort _} {f : ι → F} {s : Finset ι} : (∏ i ∈ s, (X - C (f i))).Separable ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
Full source 
theorem separable_prod_X_sub_C_iff' {ι : Sort _} {f : ι → F} {s : Finset ι} :
    (∏ i ∈ s, (X - C (f i))).Separable ↔ ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y :=
  ⟨fun hfs _ hx _ hy hfxy => hfs.inj_of_prod_X_sub_C hx hy hfxy, fun H => by
    rw [← prod_attach]
    exact
      separable_prod'
        (fun x _hx y _hy hxy =>
          @pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (fun x => f x)
            (fun x y hxy => Subtype.eq <| H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
        fun _ _ => separable_X_sub_C⟩
Separability of Product of Linear Factors $\prod_{i \in s} (X - f(i))$ is Equivalent to Injectivity of $f$ on $s$
Informal description
Let $F$ be a field, $\iota$ a type, $f \colon \iota \to F$ a function, and $s$ a finite subset of $\iota$. The product $\prod_{i \in s} (X - f(i))$ is separable if and only if for any $x, y \in s$, if $f(x) = f(y)$ then $x = y$.
Polynomial.separable_prod_X_sub_C_iff theorem
{ι : Sort _} [Fintype ι] {f : ι → F} : (∏ i, (X - C (f i))).Separable ↔ Function.Injective f
Full source 
theorem separable_prod_X_sub_C_iff {ι : Sort _} [Fintype ι] {f : ι → F} :
    (∏ i, (X - C (f i))).Separable ↔ Function.Injective f :=
  separable_prod_X_sub_C_iff'.trans <| by simp_rw [mem_univ, true_imp_iff, Function.Injective]
Separability of $\prod_{i} (X - f(i))$ is equivalent to injectivity of $f$
Informal description
Let $F$ be a field and $\iota$ a finite type. For a function $f \colon \iota \to F$, the product $\prod_{i \in \iota} (X - f(i))$ is separable if and only if $f$ is injective.
Polynomial.separable_or theorem
{f : F[X]} (hf : Irreducible f) : f.Separable ∨ ¬f.Separable ∧ ∃ g : F[X], Irreducible g ∧ expand F p g = f
Full source 
theorem separable_or {f : F[X]} (hf : Irreducible f) :
    f.Separable ∨ ¬f.Separable ∧ ∃ g : F[X], Irreducible g ∧ expand F p g = f := by
  classical
  exact if H : derivative f = 0 then by
    rcases p.eq_zero_or_pos with (rfl | hp)
    · haveI := CharP.charP_to_charZero F
      have := natDegree_eq_zero_of_derivative_eq_zero H
      have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
      contradiction
    haveI := isLocalHom_expand F hp
    exact
      Or.inr
        ⟨by rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H], contract p f,
          Irreducible.of_map (by rwa [← expand_contract p H hp.ne'] at hf),
          expand_contract p H hp.ne'⟩
  else Or.inl <| (separable_iff_derivative_ne_zero hf).2 H
Separability Dichotomy for Irreducible Polynomials in Positive Characteristic
Informal description
Let $F$ be a field of characteristic $p$ and $f \in F[X]$ be an irreducible polynomial. Then either $f$ is separable, or $f$ is not separable and there exists an irreducible polynomial $g \in F[X]$ such that $f(X) = g(X^p)$.
Polynomial.exists_separable_of_irreducible theorem
{f : F[X]} (hf : Irreducible f) (hp : p ≠ 0) : ∃ (n : ℕ) (g : F[X]), g.Separable ∧ expand F (p ^ n) g = f
Full source 
theorem exists_separable_of_irreducible {f : F[X]} (hf : Irreducible f) (hp : p ≠ 0) :
    ∃ (n : ℕ) (g : F[X]), g.Separable ∧ expand F (p ^ n) g = f := by
  replace hp : p.Prime := (CharP.char_is_prime_or_zero F p).resolve_right hp
  induction' hn : f.natDegree using Nat.strong_induction_on with N ih generalizing f
  rcases separable_or p hf with (h | ⟨h1, g, hg, hgf⟩)
  · refine ⟨0, f, h, ?_⟩
    rw [pow_zero, expand_one]
  · rcases N with - | N
    · rw [natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff] at hn
      rw [hn, separable_C, isUnit_iff_ne_zero, Classical.not_not] at h1
      have hf0 : f ≠ 0 := hf.ne_zero
      rw [h1, C_0] at hn
      exact absurd hn hf0
    have hg1 : g.natDegree * p = N.succ := by rwa [← natDegree_expand, hgf]
    have hg2 : g.natDegree ≠ 0 := by
      intro this
      rw [this, zero_mul] at hg1
      cases hg1
    have hg3 : g.natDegree < N.succ := by
      rw [← mul_one g.natDegree, ← hg1]
      exact Nat.mul_lt_mul_of_pos_left hp.one_lt hg2.bot_lt
    rcases ih _ hg3 hg rfl with ⟨n, g, hg4, rfl⟩
    refine ⟨n + 1, g, hg4, ?_⟩
    rw [← hgf, expand_expand, pow_succ']
Existence of Separable Expansion for Irreducible Polynomials in Nonzero Characteristic
Informal description
Let $F$ be a field of characteristic $p \neq 0$ and $f \in F[X]$ be an irreducible polynomial. Then there exists a natural number $n$ and a separable polynomial $g \in F[X]$ such that $f(X) = g(X^{p^n})$.
Polynomial.isUnit_or_eq_zero_of_separable_expand theorem
{f : F[X]} (n : ℕ) (hp : 0 < p) (hf : (expand F (p ^ n) f).Separable) : IsUnit f ∨ n = 0
Full source 
theorem isUnit_or_eq_zero_of_separable_expand {f : F[X]} (n : ℕ) (hp : 0 < p)
    (hf : (expand F (p ^ n) f).Separable) : IsUnitIsUnit f ∨ n = 0 := by
  rw [or_iff_not_imp_right]
  rintro hn : n ≠ 0
  have hf2 : derivative (expand F (p ^ n) f) = 0 := by
    rw [derivative_expand, Nat.cast_pow, CharP.cast_eq_zero, zero_pow hn, zero_mul, mul_zero]
  rw [separable_def, hf2, isCoprime_zero_right, isUnit_iff] at hf
  rcases hf with ⟨r, hr, hrf⟩
  rw [eq_comm, expand_eq_C (pow_pos hp _)] at hrf
  rwa [hrf, isUnit_C]
Unit or Zero Exponent for Separable Expansion of Polynomials in Positive Characteristic
Informal description
Let $F$ be a field of characteristic $p > 0$, and let $f \in F[X]$ be a polynomial. If the expansion $f(X^{p^n})$ is separable for some natural number $n$, then either $f$ is a unit in $F[X]$ or $n = 0$.
Polynomial.unique_separable_of_irreducible theorem
{f : F[X]} (hf : Irreducible f) (hp : 0 < p) (n₁ : ℕ) (g₁ : F[X]) (hg₁ : g₁.Separable) (hgf₁ : expand F (p ^ n₁) g₁ = f) (n₂ : ℕ) (g₂ : F[X]) (hg₂ : g₂.Separable) (hgf₂ : expand F (p ^ n₂) g₂ = f) : n₁ = n₂ ∧ g₁ = g₂
Full source 
theorem unique_separable_of_irreducible {f : F[X]} (hf : Irreducible f) (hp : 0 < p) (n₁ : ℕ)
    (g₁ : F[X]) (hg₁ : g₁.Separable) (hgf₁ : expand F (p ^ n₁) g₁ = f) (n₂ : ℕ) (g₂ : F[X])
    (hg₂ : g₂.Separable) (hgf₂ : expand F (p ^ n₂) g₂ = f) : n₁ = n₂ ∧ g₁ = g₂ := by
  revert g₁ g₂
  wlog hn : n₁ ≤ n₂
  · intro g₁ hg₁ Hg₁ g₂ hg₂ Hg₂
    simpa only [eq_comm] using this p hf hp n₂ n₁ (le_of_not_le hn) g₂ hg₂ Hg₂ g₁ hg₁ Hg₁
  have hf0 : f ≠ 0 := hf.ne_zero
  intros g₁ hg₁ hgf₁ g₂ hg₂ hgf₂
  rw [le_iff_exists_add] at hn
  rcases hn with ⟨k, rfl⟩
  rw [← hgf₁, pow_add, expand_mul, expand_inj (pow_pos hp n₁)] at hgf₂
  subst hgf₂
  subst hgf₁
  rcases isUnit_or_eq_zero_of_separable_expand p k hp hg₁ with (h | rfl)
  · rw [isUnit_iff] at h
    rcases h with ⟨r, hr, rfl⟩
    simp_rw [expand_C] at hf
    exact absurd (isUnit_C.2 hr) hf.1
  · rw [add_zero, pow_zero, expand_one]
    constructor <;> rfl
Uniqueness of Separable Expansion for Irreducible Polynomials in Positive Characteristic
Informal description
Let $F$ be a field of characteristic $p > 0$, and let $f \in F[X]$ be an irreducible polynomial. Suppose there exist natural numbers $n_1, n_2$ and separable polynomials $g_1, g_2 \in F[X]$ such that $f(X) = g_1(X^{p^{n_1}}) = g_2(X^{p^{n_2}})$. Then $n_1 = n_2$ and $g_1 = g_2$.
Polynomial.separable_X_pow_sub_C theorem
{n : ℕ} (a : F) (hn : (n : F) ≠ 0) (ha : a ≠ 0) : Separable (X ^ n - C a)
Full source 
/-- If `n ≠ 0` in `F`, then `X ^ n - a` is separable for any `a ≠ 0`. -/
theorem separable_X_pow_sub_C {n : ℕ} (a : F) (hn : (n : F) ≠ 0) (ha : a ≠ 0) :
    Separable (X ^ n - C a) :=
  separable_X_pow_sub_C_unit (Units.mk0 a ha) (IsUnit.mk0 (n : F) hn)
Separability of $X^n - a$ when $n$ is invertible in $F$
Informal description
Let $F$ be a field, $n$ a natural number, and $a \in F$ a nonzero element. If the image of $n$ in $F$ is nonzero (i.e., the characteristic of $F$ does not divide $n$), then the polynomial $X^n - a$ is separable over $F$.
Polynomial.separable_X_pow_sub_C' theorem
(p n : ℕ) (a : F) [CharP F p] (hn : ¬p ∣ n) (ha : a ≠ 0) : Separable (X ^ n - C a)
Full source 
/-- If `F` is of characteristic `p` and `p ∤ n`, then `X ^ n - a` is separable for any `a ≠ 0`. -/
theorem separable_X_pow_sub_C' (p n : ℕ) (a : F) [CharP F p] (hn : ¬p ∣ n) (ha : a ≠ 0) :
    Separable (X ^ n - C a) :=
  separable_X_pow_sub_C a (by rwa [← CharP.cast_eq_zero_iff F p n] at hn) ha
Separability of $X^n - a$ in characteristic $p$ when $p \nmid n$ and $a \neq 0$
Informal description
Let $F$ be a field of characteristic $p$, and let $n$ be a natural number not divisible by $p$. For any nonzero element $a \in F$, the polynomial $X^n - a$ is separable over $F$.
Polynomial.X_pow_sub_one_separable_iff theorem
{n : ℕ} : (X ^ n - 1 : F[X]).Separable ↔ (n : F) ≠ 0
Full source 
/-- In a field `F`, `X ^ n - 1` is separable iff `↑n ≠ 0`. -/
theorem X_pow_sub_one_separable_iff {n : ℕ} : (X ^ n - 1 : F[X]).Separable ↔ (n : F) ≠ 0 := by
  refine ⟨?_, fun h => separable_X_pow_sub_C_unit 1 (IsUnit.mk0 _ h)⟩
  rw [separable_def', derivative_sub, derivative_X_pow, derivative_one, sub_zero]
  -- Suppose `(n : F) = 0`, then the derivative is `0`, so `X ^ n - 1` is a unit, contradiction.
  rintro (h : IsCoprime _ _) hn'
  rw [hn', C_0, zero_mul, isCoprime_zero_right] at h
  exact not_isUnit_X_pow_sub_one F n h
Separability of $X^n - 1$ iff $n \neq 0$ in $F$
Informal description
For any natural number $n$ and field $F$, the polynomial $X^n - 1$ is separable over $F$ if and only if the image of $n$ in $F$ is nonzero (i.e., $n \neq 0$ in $F$).
Polynomial.card_rootSet_eq_natDegree theorem
[Algebra F K] {p : F[X]} (hsep : p.Separable) (hsplit : Splits (algebraMap F K) p) : Fintype.card (p.rootSet K) = p.natDegree
Full source 
theorem card_rootSet_eq_natDegree [Algebra F K] {p : F[X]} (hsep : p.Separable)
    (hsplit : Splits (algebraMap F K) p) : Fintype.card (p.rootSet K) = p.natDegree := by
  classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe]
  rw [Multiset.toFinset_card_of_nodup (nodup_roots hsep.map), ← natDegree_eq_card_roots hsplit]
Number of Distinct Roots Equals Degree for Separable Splitting Polynomials
Informal description
Let $F$ and $K$ be fields with an algebra structure $F \to K$, and let $p$ be a separable polynomial over $F$ that splits completely over $K$ via the algebra map. Then the number of distinct roots of $p$ in $K$ equals the degree of $p$, i.e., $|\text{rootSet}_K(p)| = \deg p$.
Polynomial.nodup_roots_iff_of_splits theorem
{f : F[X]} (hf : f ≠ 0) (h : f.Splits (RingHom.id F)) : f.roots.Nodup ↔ f.Separable
Full source 
/-- If a non-zero polynomial splits, then it has no repeated roots on that field
if and only if it is separable. -/
theorem nodup_roots_iff_of_splits {f : F[X]} (hf : f ≠ 0) (h : f.Splits (RingHom.id F)) :
    f.roots.Nodup ↔ f.Separable := by
  classical
  refine ⟨(fun hnsep ↦ ?_).mtr, nodup_roots⟩
  rw [Separable, ← gcd_isUnit_iff, isUnit_iff_degree_eq_zero] at hnsep
  obtain ⟨x, hx⟩ := exists_root_of_splits _
    (splits_of_splits_of_dvd _ hf h (gcd_dvd_left f _)) hnsep
  simp_rw [Multiset.nodup_iff_count_le_one, not_forall, not_le]
  exact ⟨x, ((one_lt_rootMultiplicity_iff_isRoot_gcd hf).2 hx).trans_eq f.count_roots.symm⟩
Distinct roots characterization of separable polynomials over a splitting field
Informal description
Let $F$ be a field and $f \in F[X]$ be a non-zero polynomial that splits over $F$. Then the multiset of roots of $f$ has no repeated elements if and only if $f$ is separable (i.e., $f$ is coprime with its derivative $f'$).
Polynomial.nodup_aroots_iff_of_splits theorem
[Algebra F K] {f : F[X]} (hf : f ≠ 0) (h : f.Splits (algebraMap F K)) : (f.aroots K).Nodup ↔ f.Separable
Full source 
/-- If a non-zero polynomial over `F` splits in `K`, then it has no repeated roots on `K`
if and only if it is separable. -/
@[stacks 09H3 "Here we only require `f` splits instead of `K` is algebraically closed."]
theorem nodup_aroots_iff_of_splits [Algebra F K] {f : F[X]} (hf : f ≠ 0)
    (h : f.Splits (algebraMap F K)) : (f.aroots K).Nodup ↔ f.Separable := by
  rw [← (algebraMap F K).id_comp, ← splits_map_iff] at h
  rw [nodup_roots_iff_of_splits (map_ne_zero hf) h, separable_map]
Distinct Roots Characterization for Separable Polynomials over Splitting Fields
Informal description
Let $F$ and $K$ be fields with an algebra structure $F \to K$, and let $f \in F[X]$ be a non-zero polynomial that splits completely over $K$ via the algebra map. Then the multiset of roots of $f$ in $K$ has no repeated elements if and only if $f$ is separable (i.e., $f$ is coprime with its derivative $f'$).
Polynomial.card_rootSet_eq_natDegree_iff_of_splits theorem
[Algebra F K] {f : F[X]} (hf : f ≠ 0) (h : f.Splits (algebraMap F K)) : Fintype.card (f.rootSet K) = f.natDegree ↔ f.Separable
Full source 
theorem card_rootSet_eq_natDegree_iff_of_splits [Algebra F K] {f : F[X]} (hf : f ≠ 0)
    (h : f.Splits (algebraMap F K)) : Fintype.cardFintype.card (f.rootSet K) = f.natDegree ↔ f.Separable := by
  classical
  simp_rw [rootSet_def, Finset.coe_sort_coe, Fintype.card_coe, natDegree_eq_card_roots h,
    Multiset.toFinset_card_eq_card_iff_nodup, nodup_aroots_iff_of_splits hf h]
Cardinality of Root Set Equals Degree if and only if Polynomial is Separable
Informal description
Let $F$ and $K$ be fields with an algebra structure $F \to K$, and let $f \in F[X]$ be a non-zero polynomial that splits completely over $K$ via the algebra map. Then the number of distinct roots of $f$ in $K$ equals the degree of $f$ if and only if $f$ is separable (i.e., $f$ is coprime with its derivative $f'$).
Polynomial.exists_finset_of_splits theorem
(i : F →+* K) {f : F[X]} (sep : Separable f) (sp : Splits i f) : ∃ s : Finset K, f.map i = C (i f.leadingCoeff) * s.prod fun a : K => X - C a
Full source 
theorem exists_finset_of_splits (i : F →+* K) {f : F[X]} (sep : Separable f) (sp : Splits i f) :
    ∃ s : Finset K, f.map i = C (i f.leadingCoeff) * s.prod fun a : K => X - C a := by
  classical
  obtain ⟨s, h⟩ := (splits_iff_exists_multiset _).1 sp
  use s.toFinset
  rw [h, Finset.prod_eq_multiset_prod, ← Multiset.toFinset_eq]
  apply nodup_of_separable_prod
  apply Separable.of_mul_right
  rw [← h]
  exact sep.map
Factorization of Separable Polynomials over Splitting Fields
Informal description
Let $F$ and $K$ be fields with a ring homomorphism $i \colon F \to K$, and let $f \in F[X]$ be a separable polynomial that splits over $K$ via $i$. Then there exists a finite subset $s \subseteq K$ such that the polynomial $f$ mapped by $i$ can be expressed as: \[ f \circ i = C(i(f_{\text{lead}})) \cdot \prod_{a \in s} (X - a), \] where $f_{\text{lead}}$ is the leading coefficient of $f$ and $C$ denotes the constant polynomial embedding.
Irreducible.separable theorem
[CharZero F] {f : F[X]} (hf : Irreducible f) : f.Separable
Full source 
theorem _root_.Irreducible.separable [CharZero F] {f : F[X]} (hf : Irreducible f) :
    f.Separable := by
  rw [separable_iff_derivative_ne_zero hf, Ne, ← degree_eq_bot, degree_derivative_eq]
  · rintro ⟨⟩
  rw [pos_iff_ne_zero, Ne, natDegree_eq_zero_iff_degree_le_zero, degree_le_zero_iff]
  refine fun hf1 => hf.not_isUnit ?_
  rw [hf1, isUnit_C, isUnit_iff_ne_zero]
  intro hf2
  rw [hf2, C_0] at hf1
  exact absurd hf1 hf.ne_zero
Irreducible polynomials over fields of characteristic zero are separable
Informal description
Let $F$ be a field of characteristic zero and $f \in F[X]$ be an irreducible polynomial. Then $f$ is separable, i.e., $f$ is coprime with its derivative $f'$.
IsSeparable definition
(x : K) : Prop
Full source 
/--
An element `x` of an algebra `K` over a commutative ring `F` is said to be *separable*, if its
minimal polynomial over `K` is separable. Note that the minimal polynomial of any element not
integral over `F` is defined to be `0`, which is not a separable polynomial.
-/
@[stacks 09H1 "second part"]
def IsSeparable (x : K) : Prop := Polynomial.Separable (minpoly F x)
Separable element in a field extension
Informal description
An element \( x \) in a field extension \( K \) over a commutative ring \( F \) is called *separable* if its minimal polynomial over \( F \) is separable, i.e., it is coprime with its derivative. Note that if \( x \) is not integral over \( F \), its minimal polynomial is defined to be \( 0 \), which is not separable.
Algebra.IsSeparable structure
Full source 
/-- Typeclass for separable field extension: `K` is a separable field extension of `F` iff
the minimal polynomial of every `x : K` is separable. This implies that `K/F` is an algebraic
extension, because the minimal polynomial of a non-integral element is `0`, which is not
separable.

We define this for general (commutative) rings and only assume `F` and `K` are fields if this
is needed for a proof. -/
@[mk_iff isSeparable_def, stacks 09H1 "third part"]
protected class Algebra.IsSeparable : Prop where
  isSeparable' : ∀ x : K, IsSeparable F x
Separable field extension
Informal description
A field extension \( L \) over \( K \) is called *separable* if every element \( x \in L \) has a separable minimal polynomial over \( K \). This implies that \( L/K \) is an algebraic extension, since the minimal polynomial of a non-integral element is \( 0 \), which is not separable. This definition is given for general commutative rings, but the assumption that \( K \) and \( L \) are fields is only used when necessary in proofs.
Algebra.IsSeparable.isSeparable theorem
[Algebra.IsSeparable F K] : ∀ x : K, IsSeparable F x
Full source 
theorem Algebra.IsSeparable.isSeparable [Algebra.IsSeparable F K] : ∀ x : K, IsSeparable F x :=
  Algebra.IsSeparable.isSeparable'
Elements in a separable extension are separable
Informal description
If $L/K$ is a separable field extension, then every element $x \in L$ is separable over $K$, meaning its minimal polynomial over $K$ is coprime with its derivative.
IsSeparable.isIntegral theorem
{x : K} (h : IsSeparable F x) : IsIntegral F x
Full source 
/-- If the minimal polynomial of `x : K` over `F` is separable, then `x` is integral over `F`,
because the minimal polynomial of a non-integral element is `0`, which is not separable. -/
theorem IsSeparable.isIntegral {x : K} (h : IsSeparable F x) : IsIntegral F x := by
  cases subsingleton_or_nontrivial F
  · haveI := Module.subsingleton F K
    exact ⟨1, monic_one, Subsingleton.elim _ _⟩
  · exact of_not_not (h.ne_zero <| minpoly.eq_zero ·)
Separability Implies Integrality in Field Extensions
Informal description
For any element $x$ in a field extension $K$ over a commutative ring $F$, if $x$ is separable over $F$ (i.e., its minimal polynomial over $F$ is separable), then $x$ is integral over $F$.
Algebra.isSeparable_iff theorem
: Algebra.IsSeparable F K ↔ ∀ x : K, IsIntegral F x ∧ IsSeparable F x
Full source 
theorem Algebra.isSeparable_iff :
    Algebra.IsSeparableAlgebra.IsSeparable F K ↔ ∀ x : K, IsIntegral F x ∧ IsSeparable F x :=
  ⟨fun _ x => ⟨Algebra.IsSeparable.isIntegral F x, Algebra.IsSeparable.isSeparable F x⟩,
    fun h => ⟨fun x => (h x).2⟩⟩
Characterization of Separable Field Extensions: $K/F$ separable $\leftrightarrow$ all elements integral and separable
Informal description
A field extension $K/F$ is separable if and only if every element $x \in K$ is integral over $F$ and its minimal polynomial over $F$ is separable (i.e., coprime with its derivative).
AlgEquiv.isSeparable_iff theorem
{x : K} : IsSeparable F (e x) ↔ IsSeparable F x
Full source 
/-- Transfer `IsSeparable` across an `AlgEquiv`. -/
theorem AlgEquiv.isSeparable_iff {x : K} : IsSeparableIsSeparable F (e x) ↔ IsSeparable F x := by
  simp only [IsSeparable, minpoly.algEquiv_eq e x]
Preservation of Separability under Algebra Isomorphism
Informal description
Let $F$ be a commutative ring and $K$, $E$ be $F$-algebras. Given an $F$-algebra isomorphism $e \colon K \to E$ and an element $x \in K$, the element $e(x)$ is separable over $F$ if and only if $x$ is separable over $F$.
AlgEquiv.Algebra.isSeparable theorem
[Algebra.IsSeparable F K] : Algebra.IsSeparable F E
Full source 
/-- Transfer `Algebra.IsSeparable` across an `AlgEquiv`. -/
theorem AlgEquiv.Algebra.isSeparable [Algebra.IsSeparable F K] : Algebra.IsSeparable F E :=
  ⟨fun _ ↦ e.symm.isSeparable_iff.mp (Algebra.IsSeparable.isSeparable _ _)⟩
Preservation of Separable Extension under Algebra Isomorphism
Informal description
Let $F$ be a commutative ring and $K$, $E$ be $F$-algebras. Given an $F$-algebra isomorphism $e \colon K \to E$, if $K$ is a separable extension of $F$, then $E$ is also a separable extension of $F$.
AlgEquiv.Algebra.isSeparable_iff theorem
: Algebra.IsSeparable F K ↔ Algebra.IsSeparable F E
Full source 
theorem AlgEquiv.Algebra.isSeparable_iff : Algebra.IsSeparableAlgebra.IsSeparable F K ↔ Algebra.IsSeparable F E :=
  ⟨fun _ ↦ AlgEquiv.Algebra.isSeparable e, fun _ ↦ AlgEquiv.Algebra.isSeparable e.symm⟩
Separability Equivalence under Algebra Isomorphism
Informal description
Let $F$ be a commutative ring and $K$, $E$ be $F$-algebras. Given an $F$-algebra isomorphism $e \colon K \to E$, the field extension $K$ is separable over $F$ if and only if $E$ is separable over $F$.
IsSeparable.tower_top theorem
{x : E} (h : IsSeparable F x) : IsSeparable L x
Full source 
/-- If `E / L / F` is a scalar tower and `x : E` is separable over `F`, then it's also separable
over `L`. -/
@[stacks 09H2 "first part"]
theorem IsSeparable.tower_top
    {x : E} (h : IsSeparable F x) : IsSeparable L x :=
  h.map.of_dvd (minpoly.dvd_map_of_isScalarTower _ _ _)
Separability in tower extensions: $F$-separable implies $L$-separable
Informal description
Let $F \subseteq L \subseteq E$ be a tower of field extensions. If an element $x \in E$ is separable over $F$, then $x$ is also separable over $L$.
Algebra.isSeparable_tower_top_of_isSeparable theorem
[Algebra.IsSeparable F E] : Algebra.IsSeparable L E
Full source 
/-- If `E / K / F` is an extension tower, `E` is separable over `F`, then it's also separable
over `K`. -/
@[stacks 09H2 "second part"]
theorem Algebra.isSeparable_tower_top_of_isSeparable [Algebra.IsSeparable F E] :
    Algebra.IsSeparable L E :=
  ⟨fun x ↦ IsSeparable.tower_top _ (Algebra.IsSeparable.isSeparable F x)⟩
Separability in tower extensions: $F$-separable implies $L$-separable for the entire extension
Informal description
Let $F \subseteq L \subseteq E$ be a tower of field extensions. If $E$ is separable over $F$, then $E$ is also separable over $L$.
isSeparable_algebraMap theorem
(x : F) : IsSeparable F (algebraMap F K x)
Full source 
theorem isSeparable_algebraMap (x : F) : IsSeparable F (algebraMap F K x) :=
  Polynomial.Separable.of_dvd (Polynomial.separable_X_sub_C (x := x))
    (minpoly.dvd F (algebraMap F K x) (by simp only [map_sub, aeval_X, aeval_C, sub_self]))
Separability of the image under the canonical algebra map
Informal description
For any element $x$ in a field $F$, the image of $x$ under the canonical algebra map $F \to K$ is separable over $F$.
Algebra.IsSeparable.of_integral instance
: Algebra.IsSeparable F K
Full source 
/-- A integral field extension in characteristic 0 is separable. -/
protected instance (priority := 100) Algebra.IsSeparable.of_integral : Algebra.IsSeparable F K :=
  ⟨_root_.IsSeparable.of_integral _⟩
Integral Field Extensions in Characteristic Zero are Separable
Informal description
For any field extension $K$ of $F$ in characteristic zero, if every element of $K$ is integral over $F$, then $K$ is a separable extension of $F$.
IsSeparable.tower_bot theorem
{x : K} (h : IsSeparable F (algebraMap K E x)) : IsSeparable F x
Full source 
/-- If `E / K / F` is a scalar tower and `algebraMap K E x` is separable over `F`, then `x` is
also separable over `F`. -/
theorem IsSeparable.tower_bot {x : K} (h : IsSeparable F (algebraMap K E x)) : IsSeparable F x :=
    have ⟨_q, hq⟩ :=
      minpoly.dvd F x
        ((aeval_algebraMap_eq_zero_iff _ _ _).mp (minpoly.aeval F ((algebraMap K E) x)))
    (Eq.mp (congrArg Separable hq) h).of_mul_left
Separability descends in field extension towers
Informal description
Let $F \subseteq K \subseteq E$ be a tower of field extensions. If the image of an element $x \in K$ under the canonical embedding $K \hookrightarrow E$ is separable over $F$, then $x$ itself is separable over $F$.
IsSeparable.of_algHom theorem
{x : E} (h : IsSeparable F (f x)) : IsSeparable F x
Full source 
theorem IsSeparable.of_algHom {x : E} (h : IsSeparable F (f x)) : IsSeparable F x := by
  let _ : Algebra E E' := RingHom.toAlgebra f.toRingHom
  haveI : IsScalarTower F E E' := IsScalarTower.of_algebraMap_eq fun x => (f.commutes x).symm
  exact h.tower_bot
Separability preserved under algebra homomorphism preimages
Informal description
Let $F \subseteq E$ and $F \subseteq E'$ be field extensions, and let $f: E \to E'$ be an $F$-algebra homomorphism. For any element $x \in E$, if $f(x)$ is separable over $F$, then $x$ is separable over $F$.
Algebra.IsSeparable.of_algHom theorem
[Algebra.IsSeparable F E'] : Algebra.IsSeparable F E
Full source 
theorem Algebra.IsSeparable.of_algHom [Algebra.IsSeparable F E'] : Algebra.IsSeparable F E :=
  ⟨fun x => (Algebra.IsSeparable.isSeparable F (f x)).of_algHom⟩
Separability preserved under algebra homomorphism domains
Informal description
Let $F \subseteq E$ and $F \subseteq E'$ be field extensions. If there exists an $F$-algebra homomorphism $f: E \to E'$ and $E'$ is separable over $F$, then $E$ is also separable over $F$.
IsSeparable.of_equiv_equiv theorem
{x : B₁} (h : IsSeparable A₁ x) : IsSeparable A₂ (e₂ x)
Full source 
lemma IsSeparable.of_equiv_equiv {x : B₁} (h : IsSeparable A₁ x) : IsSeparable A₂ (e₂ x) :=
  letI := e₁.toRingHom.toAlgebra
  letI : Algebra A₂ B₁ :=
    { (algebraMap A₁ B₁).comp e₁.symm.toRingHom with
        algebraMap := (algebraMap A₁ B₁).comp e₁.symm.toRingHom
        smul := fun a b ↦ ((algebraMap A₁ B₁).comp e₁.symm.toRingHom a) * b
        commutes' := fun r x ↦ (Algebra.commutes) (e₁.symm.toRingHom r) x
        smul_def' := fun _ _ ↦ rfl }
  haveI : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq <| fun x ↦
      (algebraMap A₁ B₁).congr_arg <| id ((e₁.symm_apply_apply x).symm)
  let e : B₁ ≃ₐ[A₂] B₂ :=
    { e₂ with
      commutes' := fun x ↦ by
        simpa [RingHom.algebraMap_toAlgebra] using DFunLike.congr_fun he.symm (e₁.symm x) }
  (AlgEquiv.isSeparable_iff e).mpr <| IsSeparable.tower_top A₂ h
Preservation of Separability under Compatible Algebra Isomorphisms
Informal description
Let $A_1$ and $A_2$ be commutative rings, and $B_1$ and $B_2$ be $A_1$- and $A_2$-algebras respectively. Given an $A_1$-algebra isomorphism $e_1 \colon A_1 \to A_2$ and an $A_2$-algebra isomorphism $e_2 \colon B_1 \to B_2$ that are compatible via $e_1$, if an element $x \in B_1$ is separable over $A_1$, then $e_2(x)$ is separable over $A_2$.
Algebra.IsSeparable.of_equiv_equiv theorem
[Algebra.IsSeparable A₁ B₁] : Algebra.IsSeparable A₂ B₂
Full source 
lemma Algebra.IsSeparable.of_equiv_equiv [Algebra.IsSeparable A₁ B₁] : Algebra.IsSeparable A₂ B₂ :=
  ⟨fun x ↦ (e₂.apply_symm_apply x) ▸ _root_.IsSeparable.of_equiv_equiv e₁ e₂ he
    (Algebra.IsSeparable.isSeparable _ _)⟩
Preservation of Separable Extension under Compatible Algebra Isomorphisms
Informal description
Let $A_1$ and $A_2$ be commutative rings, and $B_1$ and $B_2$ be $A_1$- and $A_2$-algebras respectively. Given an $A_1$-algebra isomorphism $e_1 \colon A_1 \to A_2$ and an $A_2$-algebra isomorphism $e_2 \colon B_1 \to B_2$ that are compatible via $e_1$, if $B_1$ is separable over $A_1$, then $B_2$ is separable over $A_2$.
AlgHom.card_of_powerBasis theorem
(pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen) (h_splits : (minpoly K pb.gen).Splits (algebraMap K L)) : @Fintype.card (S →ₐ[K] L) (PowerBasis.AlgHom.fintype pb) = pb.dim
Full source 
theorem AlgHom.card_of_powerBasis (pb : PowerBasis K S) (h_sep : IsSeparable K pb.gen)
    (h_splits : (minpoly K pb.gen).Splits (algebraMap K L)) :
    @Fintype.card (S →ₐ[K] L) (PowerBasis.AlgHom.fintype pb) = pb.dim := by
  classical
  let _ := (PowerBasis.AlgHom.fintype pb : Fintype (S →ₐ[K] L))
  rw [Fintype.card_congr pb.liftEquiv', Fintype.card_of_subtype _ (fun x => Multiset.mem_toFinset),
    ← pb.natDegree_minpoly, natDegree_eq_card_roots h_splits, Multiset.toFinset_card_of_nodup]
  exact nodup_roots ((separable_map (algebraMap K L)).mpr h_sep)
Cardinality of Algebra Homomorphisms Equals Power Basis Dimension for Separable Extensions
Informal description
Let $K$ be a field and $S$ a $K$-algebra with a power basis $\mathrm{pb}$. Suppose the generator $\mathrm{pb.gen}$ is separable over $K$ (i.e., its minimal polynomial is separable) and the minimal polynomial splits completely in $L$ via the algebra map $K \to L$. Then the number of $K$-algebra homomorphisms from $S$ to $L$ is equal to the dimension of the power basis, i.e., \[ |\mathrm{Hom}_K(S, L)| = \mathrm{pb.dim}. \]