mem_powers

Mathlib.Algebra.Group.Submonoid.Membership

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

English

The element n belongs to the submonoid generated by n.

Русский

Элемент n принадлежит подмономиоду, сгенерированному n.

LaTeX

$$$ n \\in \\mathrm{powers}(n) $$$

Lean4

theorem mem_powers (n : M) : n ∈ powers n :=
  ⟨1, pow_one _⟩

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

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

Разделы

Аффилиация

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