algebraMap_elemReduct_eq' — Mathlib

English

Variant: algebraMap K L (elemReduct K a) = a^{p^{elemExponent K a}}; equivalently the same relation with the p-variant.

Русский

Вариант: algebraMap K L (elemReduct K a) = a^{p^{elemExponent K a}}; эквивалентно той же связке с p-variant.

LaTeX

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

Lean4

/-- Version of `algebraMap_elemReduct_eq` using `ExpChar`. -/
theorem algebraMap_elemReduct_eq' (p : ℕ) [ExpChar K p] (a : L) :
    algebraMap K L (elemReduct K a) = a ^ p ^ elemExponent K a :=
  ringExpChar.eq K p ▸ algebraMap_elemReduct_eq K a

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