instCharZero — Mathlib

English

If R has characteristic zero, then MvPolynomial σ R also has characteristic zero.

Русский

Если характеристика R равна нулю, то и характеристика MvPolynomial(σ,R) равна нулю.

LaTeX

$$$[\\text{CharZero} \\\\ R] \\Rightarrow [\\text{CharZero}(\\mathrm{MvPolynomial}(\\sigma,R))]$$$

Lean4

instance [CharZero R] : CharZero (MvPolynomial σ R) where
  cast_injective x y hxy := by rwa [← C_eq_coe_nat, ← C_eq_coe_nat, C_inj, Nat.cast_inj] at hxy

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