pow_mem

Mathlib.FieldTheory.IntermediateField.Basic

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

English

Let S be an intermediate field of L over K. If x ∈ S, then x^n ∈ S for every natural number n.

Русский

Пусть S — промежутое поле L над K. Тогда если x ∈ S, то x^n ∈ S для любого натурального n.

LaTeX

$$$\forall x \in S:\ \forall n ∈ \mathbb{N}: x^n ∈ S$$$

Lean4

protected theorem pow_mem {x : L} (hx : x ∈ S) (n : ℤ) : x ^ n ∈ S :=
  zpow_mem hx n

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

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

Разделы

Аффилиация

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