elemExponent_min — Mathlib

English

If n is less than the exponent of a, then a^{ringExpChar(K)^{n}} is not in the base-field range.

Русский

Если n < elemExponent(K,a), то a^{ringExpChar(K)^{n}} не лежит в образе алгебраMap_KL.

LaTeX

$$$ n < \operatorname{elemExponent}(K,a) \Rightarrow a^{\operatorname{ringExpChar}(K)^{n}} \notin \operatorname{range}(\operatorname{algebraMap} K L) $$$

Lean4

theorem elemExponent_min {a : L} {n : ℕ} (h : n < elemExponent K a) : a ^ ringExpChar K ^ n ∉ (algebraMap K L).range :=
  fun hn ↦ (Nat.not_lt_of_ge <| elemExponent_le_of_pow_mem hn) h

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