hasExponent_iff' — Mathlib

English

HasExponent K L iff there exists e such that for all a ∈ L, a^{p^e} lies in the range of algebraMap K L.

Русский

Существует e такой, что для всех a ∈ L выполняется a^{p^e} ∈ образ алгебраMap K L; тогда HasExponent K L эквивалентно этому.

LaTeX

$$HasExponent K L ⇔ ∃ e ∈ ℕ, ∀ a ∈ L, a^{p^e} ∈ \operatorname{range}(\operatorname{algebraMap} K L)$$

Lean4

/-- Version of `hasExponent_iff` using `ExpChar`. -/
theorem hasExponent_iff' (p : ℕ) [ExpChar K p] : HasExponent K L ↔ ∃ e, ∀ (a : L), a ^ p ^ e ∈ (algebraMap K L).range :=
  ringExpChar.eq K p ▸ hasExponent_iff K L

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