iterate_frobenius_mk — Mathlib

English

Applying the p-th Frobenius map n times to the element mk(K,p)(⟨n,x⟩) yields the image of x under the embedding.

Русский

Применение p-й итерации Фробениуса к элементу mk(K,p)(⟨n,x⟩) даёт образ x через встроение.

LaTeX

$$$(\mathrm{frobenius}(\mathrm{PerfectClosure}(K,p),p))^{[n]}(\mathrm{mk}(K,p)\langle n,x\rangle)=\mathrm{of}(K,p)(x).$$$

Lean4

@[simp]
theorem iterate_frobenius_mk (n : ℕ) (x : K) : (frobenius (PerfectClosure K p) p)^[n] (mk K p ⟨n, x⟩) = of K p x := by
  induction n with
  | zero => rfl
  | succ n ih => rw [iterate_succ_apply, ← ih, frobenius_mk, mk_succ_pow]

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