pow_mem

Mathlib.Algebra.Group.Subgroup.Defs

URI: https://scilib.ai/kg/mathlib#Subgroup.pow_mem

English

If x ∈ K, then for all n ∈ N, x^n ∈ K.

Русский

Если x ∈ K, то для всех n ∈ ℕ выполняется x^n ∈ K.

LaTeX

$$$x \\in K \\Rightarrow \\forall n \\in \\mathbb{N}, x^n \\in K$$$

Lean4

@[to_additive]
protected theorem pow_mem {x : G} (hx : x ∈ K) : ∀ n : ℕ, x ^ n ∈ K :=
  pow_mem hx

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

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

Разделы

Аффилиация

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