addOrderOf_one

Mathlib.GroupTheory.OrderOfElement

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

English

For any ring R, the additive order of 1_R equals the characteristic of R: CharP R (addOrderOf(1)).

Русский

Для кольца R порядок сложения единицы равен характеристике: CharP R (addOrderOf(1)).

LaTeX

$$CharP R (\operatorname{addOrderOf}(1))$$

Lean4

theorem addOrderOf_one : CharP R (addOrderOf (1 : R)) where
  cast_eq_zero_iff n := by rw [← Nat.smul_one_eq_cast, addOrderOf_dvd_iff_nsmul_eq_zero]

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

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

Разделы

Аффилиация

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