charZero_of_right

Mathlib.Algebra.CharP.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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