Basic Properties of Primitive Root and Order Function
Na Ma, Xiquan Liang · Formalized Mathematics · 2012
Summary In this paper we defined the reduced residue system and proved its fundamental properties. Then we proved the basic properties of the order function. Finally, we defined the primitive root and proved its fundamental properties. Our work is based on [12], [8], and [11].