powers_le

Mathlib.Algebra.Group.Submonoid.Membership

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

English

For any n and submonoid P, powers(n) ≤ P iff n ∈ P.

Русский

Для любого n и подмоноида P, powers(n) ≤ P эквивалентно n ∈ P.

LaTeX

$$$\\mathrm{powers}(n) \\\\le P \\\\iff n \\\\in P$$$

Lean4

theorem powers_le {n : M} {P : Submonoid M} : powers n ≤ P ↔ n ∈ P := by simp [powers_eq_closure]

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

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

Разделы

Аффилиация

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