Near solutions of polynomial equations
We reformulate more explicitly the results of Momose, Ribet and Papier concerning the images of the Galois representations attached to newforms without complex multiplication, restricted to the case of weight and trivial nebentypus. We compute two examples of these newforms, with a single inner twist, and we prove that for every inert prime greater than the image is as large as possible. As a consequence, we prove that the groups for every prime , and for every prime , are Galois groups...
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].