eq

Mathlib.Algebra.CharP.Defs

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

English

If p is a natural number with CharP R p, then ringChar R = p.

Русский

Если p имеет CharP на R, то ringChar R = p.

LaTeX

$$$(p) [C : CharP R p] \Rightarrow \text{ringChar}(R) = p$$$

Lean4

theorem eq (p : ℕ) [C : CharP R p] : ringChar R = p :=
  ((Classical.choose_spec (CharP.existsUnique R)).2 p C).symm

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

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

Разделы

Аффилиация

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