gcd (a ^ m - 1) (a ^ n - 1) = a ^ gcd m n - 1

Stream: Is there code for X?

[Jiatong Yang]

Is there code for:
gcd (a ^ m - 1) (a ^ n - 1) = a ^ gcd m n - 1

[Aaron Liu]

Closest thing I could find is docs#nat_pow_one_sub_dvd_pow_mul_sub_one

[Thomas Browning]

Here's a PR: #22889

[Antoine Chambert-Loir]

It's worth being generalized: the method proves that in any (commutative) ring, the ideal generated by $a ^ m - 1$ and $a ^ n - 1$ is generated by $a ^ d - 1$, for $d = \gcd(m,n)$.