pow_mem

Mathlib.FieldTheory.IsPerfectClosure

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

English

In an IsPRadical setting, for x ∈ L there exists n and y ∈ K with i(y) = x^{p^n}.

Русский

В рамках IsPRadical для x ∈ L существует n и y ∈ K такие, что i(y) = x^{p^n}.

LaTeX

$$$$ \\exists n,\\; \\exists y:\\K,\\; i(y)=x^{p^{n}}. $$$$

Lean4

theorem pow_mem [IsPRadical i p] (x : L) : ∃ (n : ℕ) (y : K), i y = x ^ p ^ n :=
  pow_mem' x

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

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

Разделы

Аффилиация

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