English
If a monoid A has an α-power operation and is such that for every nonzero n ∈ α the map a ↦ a^n is surjective, then every such power map is surjective.
Русский
Если моноид A имеет операцию возведения в степень α и для каждого ненулевого n ∈ α отображение a ↦ a^n сюръективно, то каждая такая карта степени сюръективна.
LaTeX
$$$\forall (A, \alpha)\,[\text{Monoid } A]\,[\text{Pow } A \alpha]\,[0 \in \alpha]\,[\text{RootableBy } A \alpha],\forall {n : \alpha}, n \neq 0 \rightarrow \text{Surjective}(a \mapsto a^n)$$$
Lean4
@[to_additive smul_right_surj_of_divisibleBy]
theorem pow_left_surj_of_rootableBy [RootableBy A α] {n : α} (hn : n ≠ 0) :
Function.Surjective (fun a => a ^ n : A → A) := fun x => ⟨RootableBy.root x n, RootableBy.root_cancel _ hn⟩
