powers_fg — Mathlib

English

For any monoid M and element r ∈ M, the submonoid generated by the powers of r is finitely generated.

Русский

Для моноида M и элемента r ∈ M подмонойд порожденный степенями r конечно порожден.

LaTeX

$$$\forall r \in M, (Submonoid.powers r).FG$$$

Lean4

@[to_additive]
theorem powers_fg (r : M) : (Submonoid.powers r).FG :=
  ⟨{ r }, (Finset.coe_singleton r).symm ▸ (Submonoid.powers_eq_closure r).symm⟩

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