charZero_of_left

Mathlib.Algebra.CharP.Basic

URI: https://scilib.ai/kg/mathlib#Prod.charZero_of_left

English

If the left factor has characteristic zero, then the product ring also has characteristic zero.

Русский

Если левая характеристика ноль, то произведение кольца также имеет характеристику ноль.

LaTeX

$$CharZero(R) ⇒ CharZero(R × S)$$

Lean4

instance charZero_of_left [CharZero R] : CharZero (R × S) where
  cast_injective _ _ h := CharZero.cast_injective congr(Prod.fst $h)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru