instCharP — Mathlib

English

For any natural p, if k has characteristic p, then AlgebraicClosure(k) has the same characteristic p.

Русский

Для любого p, если характеристика k равна p, то характеристика AlgebraicClosure(k) тоже равна p.

LaTeX

$$$\text{CharP}(k,p) \Rightarrow \text{CharP}(\text{AlgebraicClosure}(k),p).$$$

Lean4

instance {p : ℕ} [CharP k p] : CharP (AlgebraicClosure k) p :=
  charP_of_injective_algebraMap (RingHom.injective (algebraMap k (AlgebraicClosure k))) p

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