charZero_of_expChar_one'

Mathlib.Algebra.CharP.Defs

URI: https://scilib.ai/kg/mathlib#charZero_of_expChar_one'

← MathLib Explorer

English

If ExpChar R 1, then CharZero R.

Русский

Если ExpChar R 1, то CharZero R.

LaTeX

$$$[ExpChar R 1] \\\\Rightarrow \\\\CharZero R$$$

Lean4

/-- The characteristic is zero if the exponential characteristic is one. -/
theorem charZero_of_expChar_one' [hq : ExpChar R 1] : CharZero R :=
  by
  cases hq
  · assumption
  · exact False.elim (CharP.char_ne_one R 1 rfl)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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