zpow_mem

Mathlib.Algebra.Field.Subfield.Defs

URI: https://scilib.ai/kg/mathlib#Subfield.zpow_mem

English

Let s ⊆ K be a subfield of a division ring K. For x ∈ s and any integer n, x^n ∈ s.

Русский

Пусть s ⊆ K — подполе. Тогда для x ∈ s и любого n ∈ ℤ выполняется x^n ∈ s.

LaTeX

$$$x \in s \Rightarrow x^n \in s$ for all $n \in \mathbb{Z}$$$

Lean4

protected theorem zpow_mem {x : K} (hx : x ∈ s) (n : ℤ) : x ^ n ∈ s :=
  zpow_mem hx n

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

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

Разделы

Аффилиация

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