elemExponent_eq_zero_of_charZero — Mathlib

English

If the base field K has characteristic zero, then elemExponent K a = 0 for all a ∈ L.

Русский

Если характеристика базового поля K равна нулю, то для любого a ∈ L имеет место elemExponent K a = 0.

LaTeX

$$elemExponent K a = 0$$

Lean4

theorem elemExponent_eq_zero_of_charZero (a : L) [CharZero K] : elemExponent K a = 0 :=
  elemExponent_eq_zero_of_mem_range <| surjective_algebraMap_of_isSeparable K L a

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