instCharZero — Mathlib

English

If the base field K has characteristic zero, then the splitting field f.SplittingField also has characteristic zero.

Русский

Если характеристика поля K равна нулю, то характеристика поля развёртывания f так же равна нулю.

LaTeX

$$$\operatorname{Char}(K)=0 \Rightarrow \operatorname{Char}(\mathrm{SplittingField}(f))=0$$$

Lean4

instance instCharZero [CharZero K] : CharZero (SplittingField f) :=
  charZero_of_injective_algebraMap (algebraMap K _).injective

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