exponent_min' — Mathlib

English

For any p and e < exponent K L, there exists a ∈ L with a^{p^e} ∉ range(algebraMap K L).

Русский

Для любого p и e < exponent K L существует a ∈ L такое, что a^{p^e} ∉ образ algebraMap K L.

LaTeX

$$∀ p, ∀ e < exponent K L, ∃ a ∈ L, a^{p^{e}} ∉ \operatorname{range}(\operatorname{algebraMap} K L)$$

Lean4

/-- Version of `exponent_min` using `ExpChar`. -/
theorem exponent_min' [HasExponent K L] (p : ℕ) [ExpChar K p] {e : ℕ} (h : e < exponent K L) :
    ∃ a, a ^ p ^ e ∉ (algebraMap K L).range :=
  ringExpChar.eq K p ▸ exponent_min h

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