charP — Mathlib

English

If R has CharP p, then FreeAlgebra R X also has CharP p.

Русский

Если R имеет характеристику p, то FreeAlgebra R X тоже имеет характеристику p.

LaTeX

$$$( \\text{CharP}(R,p) ) \\Rightarrow \\text{CharP}(\\mathrm{FreeAlgebra}(R,X), p)$$$

Lean4

/-- If `R` has characteristic `p`, then so does `FreeAlgebra R X`. -/
instance charP [CharP R p] : CharP (FreeAlgebra R X) p :=
  charP_of_injective_algebraMap FreeAlgebra.algebraMap_leftInverse.injective p

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