lift_aux

Mathlib.FieldTheory.IsPerfectClosure

URI: https://scilib.ai/kg/mathlib#PerfectRing.lift_aux

English

For x ∈ L, there exist n ∈ ℕ and y ∈ K such that i(y) = x^(p^n).

Русский

Для каждого x ∈ L существуют n ∈ ℕ и y ∈ K такие, что i(y) = x^(p^n).

LaTeX

$$$\\exists n \\in \\mathbb{N}, \\exists y \\in K, i(y) = x^{p^n}$$$

Lean4

theorem lift_aux (x : L) : ∃ y : ℕ × K, i y.2 = x ^ p ^ y.1 :=
  by
  obtain ⟨n, y, h⟩ := IsPRadical.pow_mem i p x
  exact ⟨(n, y), h⟩

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

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

Разделы

Аффилиация

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