charP_zero_iff_charZero

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#CharP.charP_zero_iff_charZero

English

CharP R 0 is equivalent to CharZero R.

Русский

CharP R 0 эквивалентна CharZero R.

LaTeX

$$$CharP(R,0) \iff CharZero(R).$$$

Lean4

theorem charP_zero_iff_charZero : CharP R 0 ↔ CharZero R :=
  ⟨fun _ ↦ charP_to_charZero R, fun _ ↦ ofCharZero R⟩

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

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

Разделы

Аффилиация

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