mem_perfectClosure_iff — Mathlib

English

An element x ∈ A belongs to the perfect closure of R in A with p if and only if there exists n ∈ ℕ with x^{p^n} ∈ image of algebraMap R A.

Русский

Элемент x ∈ A принадлежит совершённому замыканию R в A с p тогда и только тогда, когда существует n ∈ ℕ такое, что x^{p^n} ∈ образ отображения алгебраMap R A.

LaTeX

$$x ∈ \operatorname{perfectClosure} R A p ↔ ∃ n ∈ ℕ, x^{p^n} ∈ \operatorname{range}(\operatorname{algebraMap} R A)$$

Lean4

theorem mem_perfectClosure_iff {x : A} : x ∈ perfectClosure R A p ↔ ∃ n : ℕ, x ^ p ^ n ∈ (algebraMap R A).rangeS :=
  Iff.rfl

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