elemExponent_def' — Mathlib

English

Using ExpChar, for any p ∈ ℕ and a ∈ L, a^{p^{elemExponent(K,a)}} also lies in the range of algebraMap_KL.

Русский

С учетом ExpChar, для любого p ∈ ℕ и a ∈ L, a^{p^{elemExponent(K,a)}} также лежит в образе algebraMap_KL.

LaTeX

$$$ a^{p^{\operatorname{elemExponent}(K,a)}} \in \operatorname{range}(\operatorname{algebraMap} \\_{} K L) $$$

Lean4

/-- Version of `elemExponent_def` using `ExpChar`. -/
theorem elemExponent_def' (p : ℕ) [ExpChar K p] (a : L) : a ^ p ^ elemExponent K a ∈ (algebraMap K L).range :=
  ringExpChar.eq K p ▸ elemExponent_def K a

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