Hopf problem: period family · core 1 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.PeriodFamily.Data.cyclic_eq_generator_pow_mo1973_18373
{n : ℕ}
[NeZero n]
(x : Multiplicative (ZMod n))
: