elemExponent_def — Mathlib

English

Let K ⊆ L be fields with L/K purely inseparable. For every a ∈ L, the element a raised to the power ringExpChar(K) raised to elemExponent(K,a) lies in the image of the base-field embedding, i.e. in Im(algebraMap_KL).

Русский

Пусть K и L — поля, содержащиеся друг в друге, и расширение L/K чисто нерасщепимо. Для всякого a ∈ L элемент a^{ringExpChar(K)^{elemExponent(K,a)}} принадлежит образу вложения алгебраMap_K_L.

LaTeX

$$$ a^{\operatorname{ringExpChar}(K)^{\operatorname{elemExponent}(K,a)}} \in \operatorname{range}(\operatorname{algebraMap} \\_{} K L) $$$

Lean4

theorem elemExponent_def (a : L) : a ^ ringExpChar K ^ elemExponent K a ∈ (algebraMap K L).range :=
  RingHom.mem_range.mpr <| ⟨_, algebraMap_elemReduct_eq K a⟩

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