powers_one — Mathlib

English

In any monoid M, the submonoid generated by the identity element 1 is the smallest possible submonoid; equivalently, Powers(1) equals the bottom submonoid.

Русский

В любом моноидe M порожденный единицей 1 подп Monoid равен минимальному подп Monoid (нижняя граница).

LaTeX

$$$ \\operatorname{powers}(1) = \\bot $$$

Lean4

theorem powers_one : powers (1 : M) = ⊥ :=
  bot_unique <| powers_le.2 <| one_mem _

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