elemReduct — Mathlib

English

The element y ∈ K such that a^{ringExpChar K}^{elemExponent K a} = algebraMap K L y; i.e., a^{p^{e}} = algebraMap_K_L(y) with e = elemExponent K a.

Русский

Элемент y ∈ K удовлетворяет a^{p^{e}} = algebraMap K L y, где e = elemExponent K a.

LaTeX

$$There exists y ∈ K with a^{p^{elemExponent K a}} = algebraMap K L y$$

Lean4

/-- The element `y` of the base field `K` such that
`a ^ ringExpChar K ^ elemExponent K a = algebraMap K L y`.
See `IsPurelyInseparable.algebraMap_elemReduct_eq`. -/
noncomputable def elemReduct (a : L) : K :=
  Classical.choose <| Nat.find_spec <| minpoly_eq_X_pow_sub_C K (ringExpChar K) a

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