powers_eq_closure

Mathlib.Algebra.Group.Submonoid.Membership

URI: https://scilib.ai/kg/mathlib#Submonoid.powers_eq_closure

English

The submonoid generated by n equals the closure of {n}.

Русский

Подмоноид, порождаемый n, равен замыканию {n}.

LaTeX

$$$\\mathrm{powers}(n) = \\mathrm{closure}\\{n\\}$$$

Lean4

theorem powers_eq_closure (n : M) : powers n = closure { n } :=
  by
  ext
  exact mem_closure_singleton.symm

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru