English
If a^{ringExpChar(K)^{n}} lies in the base-field range for some n, then the exponent of a is at most n.
Русский
Если a^{ringExpChar(K)^{n}} лежит в образе алгебраMap_KL для некоторого n, то elemExponent(K,a) ≤ n.
LaTeX
$$$ a^{\operatorname{ringExpChar}(K)^{n}} \in \operatorname{range}(\operatorname{algebraMap} K L) \Rightarrow \operatorname{elemExponent}(K,a) \le n $$$
Lean4
theorem elemExponent_le_of_pow_mem {a : L} {n : ℕ} (h : a ^ ringExpChar K ^ n ∈ (algebraMap K L).range) :
elemExponent K a ≤ n := by
let ⟨p, _⟩ := ExpChar.exists K
rcases ‹ExpChar K p› with _ | ⟨hp⟩
· exact elemExponent_eq_zero_of_charZero K a ▸ Nat.zero_le _
· obtain ⟨y, hy⟩ := RingHom.mem_range.mp <| h
let f := X ^ ringExpChar K ^ n - C y
have hf₁ : f.aeval a = 0 := by rwa [map_sub, aeval_C, aeval_X_pow, sub_eq_zero, eq_comm]
have hf₂ : f.Monic := monic_X_pow_sub_C y <| Nat.pos_iff_ne_zero.mp <| expChar_pow_pos K _ _
have hf₃ : f.natDegree = ringExpChar K ^ n := by rw [natDegree_sub_C, natDegree_pow, natDegree_X, mul_one]
exact
(Nat.pow_le_pow_iff_right <| Nat.Prime.one_lt hp).mp <|
ringExpChar.eq K p ▸ hf₃ ▸ minpoly_natDegree_eq K a ▸ natDegree_le_natDegree (minpoly.min K a hf₂ hf₁)
