pow_mem — Mathlib

English

If E/F is purely inseparable, then for any x ∈ E there exists n with x^{q^n} ∈ F via the range.

Русский

Если E/F чисто безразделимо, то для любого x ∈ E найдется n такое, что x^{q^n} принадлежит F.

LaTeX

$$$ \exists n, x^{q^n} \in (\mathrm{algebraMap} F E).\mathrm{range} $$$

Lean4

theorem pow_mem [IsPurelyInseparable F E] : ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range :=
  (isPurelyInseparable_iff_pow_mem F q).1 ‹_› x

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