Exponentials at purely imaginary rational arguments

Correctly rounding trigonometric functions requires excluding exact rational boundaries. The real-exponential argument extends to imaginary integer arguments by using Gaussian integers. The polynomial X² + m² supplies both conjugate roots to mathlib's exponential approximation theorem, and a nonzero Gaussian integer has complex norm at least one.

theorem FloatLib.Numerics.Enclosure.int_add_sum_exp_intCast_mul_I_ne_zero {ι : Type u_1} (s : Finset ι) (argument : ι → ℤ) (hargument : ∀ k ∈ s, argument k ≠ 0) (a : ι → ℤ) (a₀ : ℤ) (ha₀ : a₀ ≠ 0) : ↑a₀ + ∑ k ∈ s, ↑(a k) * Complex.exp (↑(argument k) * Complex.I) ≠ 0

An integer linear combination of exponentials at nonzero imaginary integer arguments cannot cancel a nonzero integer constant.

theorem FloatLib.Numerics.Enclosure.transcendental_int_exp_intCast_mul_I (m : ℤ) (hm : m ≠ 0) : Transcendental ℤ (Complex.exp (↑m * Complex.I))

The exponential at a nonzero imaginary integer argument is transcendental over ℤ.

theorem FloatLib.Numerics.Enclosure.transcendental_exp_intCast_mul_I (m : ℤ) (hm : m ≠ 0) : Transcendental ℚ (Complex.exp (↑m * Complex.I))

The exponential at a nonzero imaginary integer argument is transcendental over ℚ.

theorem FloatLib.Numerics.Enclosure.transcendental_exp_ratCast_mul_I (q : ℚ) (hq : q ≠ 0) : Transcendental ℚ (Complex.exp (↑q * Complex.I))

The exponential at a nonzero imaginary rational argument is transcendental over ℚ.