There are several commutativity theorems in groups and rings which involve power maps f(x) = xn. The most famous example of this kind is Jacobson's theorem which asserts that any ring satisfying the identity xn = x is commutative. Such statements belong to first order logic with equality and hence provable, in principle, by any first-order theorem-prover. However, because of the presence of an arbitrary integer parameter n in the exponent, they are outside the scope of any first-order theorem-prover. In particular, one cannot use such an automated reasoning system to prove theorems involving power maps. Here we focus just on the needed properties of power maps f(x) = xn and show how one can avoid having to reason explicitly with integer exponents. Implementing these new equational properties of power maps, we show how a theorem-prover can be a handy tool for quickly proving or confirming the truth of such theorems.
@article{8751,
title = {Commutativity Theorems in Groups with Power-like Maps},
journal = {Journal of Formalized Reasoning},
volume = {12},
year = {2019},
doi = {10.6092/issn.1972-5787/8751},
language = {EN},
url = {http://dml.mathdoc.fr/item/8751}
}
Padmanabhan, Ranganathan; Zhang, Yang. Commutativity Theorems in Groups with Power-like Maps. Journal of Formalized Reasoning, Tome 12 (2019) . doi : 10.6092/issn.1972-5787/8751. http://gdmltest.u-ga.fr/item/8751/