instCharP — Mathlib

English

PerfectClosure(K, p) carries a p-th characteristic, i.e., CharP(PPerfectClosure(K, p), p) holds for the prime p and p-th characteristic in the base field lifts to the closure.

Русский

PerfectClosure(K, p) имеет характер p, то есть CharP(PerfectClosure(K, p), p) выполняется.

LaTeX

$$$\\text{CharP}(\\mathrm{PerfectClosure}\\,K\\,p, p)$$$

Lean4

instance instCharP : CharP (PerfectClosure K p) p := by
  constructor; intro x; rw [← CharP.cast_eq_zero_iff K]
  rw [← Nat.cast_zero, natCast_eq_iff, Nat.cast_zero]

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