instCharP — Mathlib

English

If the coefficient ring R has characteristic p, then the multivariate polynomial ring MvPolynomial σ R also has characteristic p.

Русский

Если характеристика кольца R равна p, то характеристика MvPolynomial(σ,R) тоже равна p.

LaTeX

$$$[\\text{CharP} \\\\ R \\\\ p] \\Rightarrow [\\text{CharP}(\\mathrm{MvPolynomial}(\\sigma,R), p)].$$$

Lean4

instance [CharP R p] : CharP (MvPolynomial σ R) p where
  cast_eq_zero_iff n := by rw [← C_eq_coe_nat, ← C_0, C_inj, CharP.cast_eq_zero_iff R p]

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