mem_perfectClosure_iff_pow_mem — Mathlib

English

A specialization: x lies in the perfect closure iff some p-power of x lies in the base field image; more generally with a fixed q (the exponential char of F).

Русский

Специализация: x ∈ совершенное замыкание тогда и только тогда, когда некоторое p-ая степень x лежит в образе элемента базового поля; далее можно заменить p на q, экспоненту F.

LaTeX

$${x ∈ perfectClosure F E} ↔ ∃ n ∈ ℕ, x^{p^n} ∈ (algebraMap F E).range$$

Lean4

theorem mem_perfectClosure_iff_pow_mem (q : ℕ) [ExpChar F q] {x : E} :
    x ∈ perfectClosure F E ↔ ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range := by
  rw [mem_perfectClosure_iff, ringExpChar.eq F q]

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