@misc{FIELD_15.MIZ,
      AUTHOR = {Schwarzweller, Christoph},
      TITLE = {Separable Polynomials and Separable Extensions},
      ADDRESS1 = {Institute of Informatics, University of Gdansk, Poland},
      SECTION1 = {Preliminaries},
      SECTION2 = {On Powers of Polynomials},
      SECTION3 = {The Rings $R^p$ for Primes $p$},
      SECTION4 = {The Polynomials $X^n - a$},
      SECTION5 = {More on Multiplicity of Roots},
      SECTION6 = {Separable Polynomials},
      SECTION7 = {Perfect Fields},
      SECTION8 = {Separable Extensions},
      DAY = {18},
      MONTH = {June},
      YEAR = {2024},
      SUMMARY = {We continue the formalization of field theory 
                 in Mizar \cite{Mizar-State-2015,BancerekJAR:2018,GrabKornSchwarz:2016}.
                 We introduce separability of polynomials and field extensions: 
                 a polynomial is separable, if it has no multiple roots in its splitting field;
                 an algebraic extension $E$ of $F$ is separable, if the minimal polynomial of
                 each $a \in E$ is separable.
                 We prove among others that a polynomial $q(X)$ is separable if and only if
                 the gcd of $q(X)$ and its (formal) derivation equals 1 -- and that a irreducible
                 polynomial $q(X)$ is separable if and only if its derivation is not 0 -- and
                 that $q(X)$ is separable if and only if the number of $q(X)$'s roots in some field 
                 extension equals the degree of $q(X)$.
                 A field $F$ is called perfect if all irreducible polynomials over $F$ are
                 separable, and as a consequence every algebraic extension of $F$ is separable.
                 Every field with characteristic 0 is perfect \cite{FIELD_14.ABS}.
                 To also consider separability in fields with prime characteristic $p$ we define
                 the rings $R^p \ = \ \{ \ a^p \ | \ a \in R \}$ and the polynomials $X^n - a$
                 for $a\in R$. Then we show that a field $F$ with prime characteristic $p$
                 is separable if and only if $F = F^p$ and that finite fields are perfect.
                 Finally we prove that for fields $F \subseteq K \subseteq E$ where $E$ is a
                 separable extension of $F$ both $E$ is separable over $K$ and $K$ is separable
                 over $F$.}}

@BOOK{Rad89,
      AUTHOR = {Radbruch, Knut},
      TITLE = {Algebra I},
      PUBLISHER = {Lecture Notes, University of Kaiserslautern, Germany},
      YEAR = {1991}}

	INTRODUCTION = {In this paper we formalize separability \cite{Lang2002} 
  using the Mizar formalism \cite{Mizar-State-2015,BancerekJAR:2018,Kornilowicz:2015:FC}. 
  A polynomial is separable, if it has no multiple roots in its splitting field;
  an algebraic extension $E$ of $F$ is separable, if the minimal polynomial of
  each $a \in E$ is separable \cite{Lunenburg1999}, \cite{Rad89}, \cite{Jac85}.\par
  In the first two sections we provide some technical lemmas necessary later.
  They concern for example divisibility and gcds of integers,
  in particular we show that a prime $p$ divides $\binom{p}{m}$ for $1 \leq m < p$.
  We also need a number of results on powers of polynomials among them
  that a polynomial $q(X)$ divides $(X-a)^n$ if and only if $q(X) = (X-a)`^l$ for some
  $0 \leq l \leq n$ or that $a$ is an $n$-fold root of $(X-a)^n$.\par
  In the third section we define the ring $R^p = \{ \ a^p \ | \ a \in R \}$ for a
  given ring $R$ with prime characteristic $p$. In order to do so we proved that 
  $(a + b)^p = a^p + b^p$, also called freshman's dream.\par
  Then we define the polynomial $q(X) = X^n - a$ necessary to describe separability in
  fields with characteristic $p \neq 0$. Note that the roots of $q(X)$ are the elements
  $b$ with $b^p = a$, so that $q(X) = (X-b)^p$ if there exists such a $b$ and
  is irreducible otherwise.\par
  In section five we deal with multiplicity of polynomials. We show among others that
  a polynomial $q(X)$ has a multiple root (in a field extension where $q(X)$ splits) if
  and only if the gcd of $q(X)$ and its (formal) derivation is not 1. For irreducible $q(X)$
  this can be sharpend to $q(X)$'s derivition being 0.
  We also prove that in fields with characteristic $p \neq 0$ the derivation of a
  polynomial $q(X)$ is 0 if and only if there exists a polynomial $r(X)$ such that 
  $q(X) = r(X^p)$.\par
  The next two sections are devoted to separability of polynomials.
  We define a polynomial $q(X)$ to be separable, if it has no multiple roots in its 
  splitting field. Note that the splitting field of $q(X)$ is unique only up to
  isomorphism, so that we had to prove that the definition indeed is independent
  of a particular splitting field.
  We prove a number of characterizations of separability found in the literature,
  for example that $q(X)$ is separable if and only if the number of $q(X)$'s roots equals
  the degree of $q(X)$ in some field extension if and only if $q(X)$ is square free in every
  field extension in which $q$ splits.
  Then we introduce perfect fields, e.g. fields in which every irreducible polynomial
  is separable. Fields with characteristic 0 are perfect (see \cite{FIELD_14.ABS}).
  Fields $F$ with characteristic $p \neq 0$ are perfect if and only if $F = F^p$.
  This is shown using the polynomial $X^p -a$, which is inseparable and irreducible
  if there is no $b$ with $b^p = a$. Because in finite fields the multiplicative
  group is cyclic in finite fields such a $b$ always exists and so finite field are 
  perfect.\par
  In the last section we define separable extensions: an algebraic extension is separable if
  the minimal polynomial of every $a \in E$ is separable. As an easy consequence we get
  that for $p(X) \in F[X] \backslash F$, where $F$ is perfect, the splitting field of 
  $p(X)$ is both normal and separable.
  We also show that for fields $F \subseteq K \subseteq E$ where $E$ is a
  separable extension of $F$ both $E$ is a separable extension of $K$ and
  $K$ is a separable extension of $F$.	}
