eq_iff

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#ringChar.eq_iff

English

For every R and p, ringChar R = p if and only if CharP R p.

Русский

Для каждого кольца R и натурального p верно: ringChar R = p тогда и только тогда, когда CharP R p.

LaTeX

$$$ringChar R = p \iff CharP R p$$$

Lean4

theorem eq_iff {p : ℕ} : ringChar R = p ↔ CharP R p :=
  ⟨of_eq, @eq R _ p⟩

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

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

Разделы

Аффилиация

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