New inequalities on polynomial divisors.
Niven’s Theorem
This article formalizes the proof of Niven’s theorem [12] which states that if x/π and sin(x) are both rational, then the sine takes values 0, ±1/2, and ±1. The main part of the formalization follows the informal proof presented at Pr∞fWiki (https://proofwiki.org/wiki/Niven’s_Theorem#Source_of_Name). For this proof, we have also formalized the rational and integral root theorems setting constraints on solutions of polynomial equations with integer coefficients [8, 9].
Norms of certain rational functions of a matrix and Schur's criterion for polynomials
Norms of matrix powers
Note sur la continuité des racines des équations algébriques
Note sur la règle des signes de Descartes