charZero_of_charZero — Mathlib

English

If R has CharZero and A is an R-algebra with FaithfulSMul, then A also has CharZero.

Русский

Если у R характеристика ноль и A является R-алгеброй с верным действием, то и A имеет CharZero.

LaTeX

$$$[CharZero\; R] \Rightarrow [CharZero\; A].$$$

Lean4

theorem charZero_of_charZero [CharZero R] : CharZero A :=
  have := algebraMap_comp_natCast R A
  ⟨this ▸ (FaithfulSMul.algebraMap_injective R A).comp CharZero.cast_injective⟩

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