powers — Mathlib

English

The submonoid generated by an element n is the set of all finite powers n^k (k ≥ 0), forming a submonoid of M.

Русский

Подмономиод, порождаемый элементом n, состоит из всех конечных степеней n^k (k ≥ 0) и образует подмономиод M.

LaTeX

$$$ \\text{powers}(n) = \\{ n^k : k \\in \\mathbb{N} \\}$ as a Submonoid of M$$

Lean4

/-- The submonoid generated by an element. -/
def powers (n : M) : Submonoid M :=
  Submonoid.copy (mrange (powersHom M n)) (Set.range (n ^ · : ℕ → M)) <|
    Set.ext fun n => exists_congr fun i => by simp; rfl

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