English
If for all n ≠ 0 the power map a ↦ a^n is surjective, then one can equip A with an α-rootable structure by taking root a n as a preimage of a under x ↦ x^n (with 1 for n = 0).
Русский
Если для всех n ≠ 0 отображение a ↦ a^n сюръективно, можно навести на A структуру α-узла: для каждого a и n определить корень как произвольный предобраз под x^n (при n = 0 берём 1).
LaTeX
$$$\text{If } \forall n \neq 0, \text{Surjective}(a \mapsto a^n) \text{, then there exists a RootableBy } A \alpha\text{ with }\text{root } a n = \begin{cases} 1, & n=0 \\ y, & n\neq 0 \text{ and } y^n = a \end{cases}$$$
Lean4
/-- A `Monoid A` is `α`-rootable iff the `pow _ n` function is surjective, i.e. the constructive version
implies the textbook approach.
-/
@[to_additive divisibleByOfSMulRightSurj /-- An `AddMonoid A` is `α`-divisible iff `n • _` is a
surjective function, i.e. the constructive version implies the textbook approach. -/
]
noncomputable def rootableByOfPowLeftSurj (H : ∀ {n : α}, n ≠ 0 → Function.Surjective (fun a => a ^ n : A → A)) :
RootableBy A α
where
root a n := @dite _ (n = 0) (Classical.dec _) (fun _ => (1 : A)) fun hn => (H hn a).choose
root_zero _ := by classical exact dif_pos rfl
root_cancel a
hn := by
dsimp only
rw [dif_neg hn]
exact (H hn a).choose_spec
