algebraMap_elemReduct_eq — Mathlib

English

The image of elemReduct under algebraMap equals a^{p^{elemExponent K a}}; i.e., algebraMap K L (elemReduct K a) = a^{ringExpChar K}^{elemExponent K a}.

Русский

Образ элемента редукции под алгебраическим отображением равен a^{p^{elemExponent K a}}; то есть algebraMap K L (elemReduct K a) = a^{ringExpChar K}^{elemExponent K a}.

LaTeX

$$algebraMap K L (elemReduct K a) = a^{ringExpChar K}^{\operatorname{elemExponent} K a}$$

Lean4

theorem algebraMap_elemReduct_eq (a : L) : algebraMap K L (elemReduct K a) = a ^ ringExpChar K ^ elemExponent K a :=
  by
  have := minpoly_eq K a ▸ minpoly.aeval K a
  rwa [map_sub, aeval_C, map_pow, aeval_X, sub_eq_zero, eq_comm] at this

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