lift_apply

Mathlib.FieldTheory.IsPerfectClosure

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

← MathLib Explorer

English

If i y = x^{p^n}, then lift x = (iterateFrobeniusEquiv M p n)^{-1}(j y).

Русский

Если i y = x^{p^n}, то lift x = (iterateFrobeniusEquiv M p n)^{-1}(j y).

LaTeX

$$lift i j p x = (iterateFrobeniusEquiv M p n)^{-1} (j y) \\quad \\text{whenever } i y = x^{p^n}$$

Lean4

theorem lift_apply (x : L) (n : ℕ) (y : K) (h : i y = x ^ p ^ n) :
    lift i j p x = (iterateFrobeniusEquiv M p n).symm (j y) :=
  liftAux_apply i j p _ _ _ h

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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