eq_one

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#ringExpChar.eq_one

English

If CharZero holds, then ringExpChar R = 1.

Русский

Если характеристика нулевая, то экспChar кольца равна 1.

LaTeX

$$$[CharZero R] \\\\Rightarrow \\\\mathrm{ringExpChar}(R) = 1$$$

Lean4

@[simp]
theorem eq_one [CharZero R] : ringExpChar R = 1 := by rw [ringExpChar, ringChar.eq_zero, max_eq_right (Nat.zero_le _)]

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

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

Разделы

Аффилиация

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