English
For any nonzero n, the map a ↦ a^n is surjective in any RootableBy A α.
Русский
Для любого ненулевого n отображение a ↦ a^n сюръективно в любой RootableBy A α.
LaTeX
$$$\forall (A : Type*) (α : Type*), [Monoid A] [Pow A α] [Zero α] [RootableBy A α], {n : α}, n \neq 0 \,\rightarrow \, \text{Surjective } (a \mapsto a^n)$$$
Lean4
/-- If `f : A → B` is a surjective homomorphism and `A` is `α`-rootable, then `B` is also `α`-rootable.
-/
@[to_additive /-- If `f : A → B` is a surjective homomorphism and `A` is `α`-divisible, then `B` is also
`α`-divisible. -/
]
noncomputable def rootableBy (hf : Function.Surjective f) (hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n) :
RootableBy B α :=
rootableByOfPowLeftSurj _ _ fun {n} hn x =>
let ⟨y, hy⟩ := hf x
⟨f <| RootableBy.root y n, (by rw [← hpow (RootableBy.root y n) n, RootableBy.root_cancel _ hn, hy] : _ ^ n = x)⟩
