coe_powers

Mathlib.Algebra.Group.Submonoid.Membership

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

English

The underlying set of powers(x) is exactly { x^n : n ∈ ℕ }. In particular, ↑(powers(x)) = { x^n : n ∈ ℕ }.

Русский

Множество, задающееся степенями x, равно множеству всех x^n, n ∈ ℕ.

LaTeX

$$$\\\\uparrow(\\\\mathrm{powers}(x)) = \\\\{ x^n \\\\mid n \\\\in \\\\mathbb{N} \\\\}$$$

Lean4

theorem coe_powers (x : M) : ↑(powers x) = Set.range fun n : ℕ => x ^ n :=
  rfl

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

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

Разделы

Аффилиация

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