Rational tangent values at rational multiples of pi

Niven's cosine theorem and the double-angle identity restrict rational tangent values to -1, 0, and 1. The other cosine cases would make a rational square equal to three. This also classifies the exact rational values of inverse tangent divided by pi.

The theorem uses mathlib's total tangent, which is zero at poles. Format operations with an invalid-result policy at poles must check for them before using this totalized value.

theorem FloatLib.Numerics.TrigonometricComparison.rational_tan_pi_mem (argument value : ℚ) (hvalue : Real.tan (↑argument * Real.pi) = ↑value) : value = -1 ∨ value = 0 ∨ value = 1

The only rational tangent values at rational multiples of pi are -1, 0, and 1.

theorem FloatLib.Numerics.TrigonometricComparison.irrational_arctan_div_pi_ratCast (argument : ℚ) (hnegative : argument ≠ -1) (hzero : argument ≠ 0) (hpositive : argument ≠ 1) : Irrational (Real.arctan ↑argument / Real.pi)

Outside the three exact inputs, inverse tangent divided by pi is irrational.