Compatible powers of a common primitive root

Represent several torsion elements as powers of one primitive root under the required order divisibility conditions.

theorem BGS.Markoff.exists_common_primitiveRoot_powers {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] (n : ℕ) [NeZero n] (w₁ w₂ w₃ : K) (hw₁ : w₁ ^ n = 1) (hw₂ : w₂ ^ n = 1) (hw₃ : w₃ ^ n = 1) : ∃ (ζ : K) (a₁ : ℕ) (a₂ : ℕ) (a₃ : ℕ), IsPrimitiveRoot ζ n ∧ a₁ < n ∧ a₂ < n ∧ a₃ < n ∧ ζ ^ a₁ = w₁ ∧ ζ ^ a₂ = w₂ ∧ ζ ^ a₃ = w₃

theorem BGS.Markoff.exists_common_primitiveRoot_powers_of_orderOf_dvd {K : Type u_1} [Field K] [IsAlgClosed K] [CharZero K] (n : ℕ) [NeZero n] (w₁ w₂ w₃ : Kˣ) (hw₁ : orderOf w₁ ∣ n) (hw₂ : orderOf w₂ ∣ n) (hw₃ : orderOf w₃ ∣ n) : ∃ (ζ : K) (a₁ : ℕ) (a₂ : ℕ) (a₃ : ℕ), IsPrimitiveRoot ζ n ∧ a₁ < n ∧ a₂ < n ∧ a₃ < n ∧ ζ ^ a₁ = ↑w₁ ∧ ζ ^ a₂ = ↑w₂ ∧ ζ ^ a₃ = ↑w₃

Three units whose exact orders divide n are simultaneous powers of one primitive n-th root. This is the group-theoretic core of the compatible cyclotomic lift.