charP_to_charZero

Mathlib.Algebra.CharP.Defs

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

English

If CharP R 0 then CharZero R.

Русский

Если CharP R 0, то CharZero R.

LaTeX

$$$[CharP(R,0)] \Rightarrow CharZero(R).$$$

Lean4

theorem charP_to_charZero [CharP R 0] : CharZero R :=
  charZero_of_inj_zero fun n h0 => eq_zero_of_zero_dvd ((cast_eq_zero_iff R 0 n).mp h0)

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

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

Разделы

Аффилиация

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