instCharP — Mathlib

English

If K has CharP p, then the splitting field f.SplittingField has CharP p as well.

Русский

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

LaTeX

$$$\operatorname{CharP}(K)=p \Rightarrow \operatorname{CharP}(\mathrm{SplittingField}(f),p)$$$

Lean4

instance instCharP (p : ℕ) [CharP K p] : CharP (SplittingField f) p :=
  charP_of_injective_algebraMap (algebraMap K _).injective p

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