English
If ζ and ζ' are primitive roots of orders k and k' (nonzero), then the product of ζ raised to k′-divided something and ζ' raised to k-divided something is a primitive root of order lcm(k,k').
Русский
Если ζ и ζ' — примитивные корни порядков k и k' (не равны нулю), то произведение соответствующих степеней даёт примитивный корень порядка lcm(k,k').
LaTeX
$$$$\text{If } \mathrm{IsPrimitiveRoot}(\zeta,k) \text{ and } \mathrm{IsPrimitiveRoot}(\zeta',k') \text{ with } k,k' \neq 0, \text{ then } \mathrm{IsPrimitiveRoot}(\zeta^{k/k_{LCM}} \cdot {\zeta'}^{k'/k'_{LCM}}, \mathrm{lcm}(k,k')).$$$$
Lean4
theorem pow_mul_pow_lcm {ζ' : M} {k' : ℕ} (hζ : IsPrimitiveRoot ζ k) (hζ' : IsPrimitiveRoot ζ' k') (hk : k ≠ 0)
(hk' : k' ≠ 0) :
IsPrimitiveRoot (ζ ^ (k / Nat.factorizationLCMLeft k k') * ζ' ^ (k' / Nat.factorizationLCMRight k k'))
(Nat.lcm k k') :=
by
convert IsPrimitiveRoot.orderOf _
convert
((Commute.all ζ ζ').orderOf_mul_pow_eq_lcm (by simpa [← hζ.eq_orderOf]) (by simpa [← hζ'.eq_orderOf])).symm using 2
all_goals simp [hζ.eq_orderOf, hζ'.eq_orderOf]
