mem_perfectClosure_iff — Mathlib

English

Membership in the perfect closure is equivalent to the existence of a power bound inside the base field's image.

Русский

Членство в совершенном замыкании эквивалентно существованию некоторого степенного элемента внутри образа базового поля.

LaTeX

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

Lean4

theorem mem_perfectClosure_iff {x : E} :
    x ∈ perfectClosure F E ↔ ∃ n : ℕ, x ^ (ringExpChar F) ^ n ∈ (algebraMap F E).range :=
  Iff.rfl

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