Schur's theorem on Galois groups of truncated exponential polynomials

Reference: (https://math.stackexchange.com/questions/2814220)

Reference (https://mathoverflow.net/questions/477077)

noncomputable def SchurTruncatedExponential.truncatedExp (n : ℕ) : Polynomial ℚ

The truncated exponential polynomial truncatedExp n is given by ∑_{j=0}^{n} x^j / j! over ℚ, which is the n-th partial sum of the Taylor series for the exponential function e^x.

Equations

• SchurTruncatedExponential.truncatedExp n = ∑ j ∈ Finset.range (n + 1), (1 / ↑j.factorial) • Polynomial.X ^ j

theorem SchurTruncatedExponential.schur_truncatedExp_galoisGroup_equiv (n : ℕ) (hn : n ≥ 2) : if n % 4 = 0 then Nonempty ((truncatedExp n).Gal ≃* ↥(alternatingGroup (Fin n))) else Nonempty ((truncatedExp n).Gal ≃* Equiv.Perm (Fin n))

Schur's Theorem (1924): Let f_n(x) = ∑_{j=0}^n x^j/j! be the n-th truncated exponential polynomial over ℚ. Then for n ≥ 2:

• If n ≡ 0 (mod 4), the Galois group of f_n is isomorphic to the alternating group A_n
• If n ≢ 0 (mod 4), the Galois group of f_n is isomorphic to the symmetric group S_n