surjective_pow — Mathlib

English

Same statement as above expressed in the standard RootableBy.surjective_pow form.

Русский

Тоже самое утверждение, выраженное через стандартную форму RootableBy.surjective_pow.

LaTeX

$$$\text{RootableBy.surjective_pow}(A,\alpha, n) : \forall n \neq 0, \text{Surjective}(a \mapsto a^n)$$$

Lean4

@[to_additive DivisibleBy.surjective_smul]
theorem surjective_pow (A α : Type*) [Monoid A] [Pow A α] [Zero α] [RootableBy A α] {n : α} (hn : n ≠ 0) :
    Function.Surjective fun a : A => a ^ n := fun a => ⟨RootableBy.root a n, RootableBy.root_cancel a hn⟩

Похожие утверждения