Theorem IsPrimitiveRoot.pow_ne_one_of_pos_of_lt

Modification history