exponent_min — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exponent_min [HasExponent K L] {e : ℕ} (h : e < exponent K L) :
    ∃ a, a ^ ringExpChar K ^ e ∉ (algebraMap K L).range :=
  not_forall.mp <| Nat.find_min ‹HasExponent K L›.has_exponent h

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