elemExponent_le_of_pow_mem' — Mathlib

English

If a^{p^{n}} lies in the base-field range for some ExpChar p, then elemExponent(K,a) ≤ n.

Русский

Если a^{p^{n}} лежит в образе алгебраMap_KL для некоторого p, то elemExponent(K,a) ≤ n.

LaTeX

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

Lean4

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

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