charP

Mathlib.Algebra.CharP.Basic

URI: https://scilib.ai/kg/mathlib#ULift.charP

← MathLib Explorer

English

If R has CharP p, then the ULift of R also has CharP p.

Русский

Если у кольца R характеристика p, то ULift R также имеетCharP p.

LaTeX

$$$ CharP\ R\ p \Rightarrow CharP\ (ULift\ R)\ p $$$

Lean4

instance charP [AddMonoidWithOne R] (p : ℕ) [CharP R p] : CharP (ULift R) p where
  cast_eq_zero_iff n := Iff.trans ULift.ext_iff <| CharP.cast_eq_zero_iff R p n

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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