false_of_nontrivial_of_char_one

Mathlib.Algebra.CharP.Defs

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

← MathLib Explorer

English

If R is a Subsingleton, then CharP R 1 holds.

Русский

Если R — subsingleton, то CharP R 1 выполняется.

LaTeX

$$Subsingleton R \Rightarrow CharP R 1$$

Lean4

theorem false_of_nontrivial_of_char_one [Nontrivial R] [CharP R 1] : False :=
  by
  have : Subsingleton R := CharOne.subsingleton
  exact false_of_nontrivial_of_subsingleton R

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

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

Разделы

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

Аффилиация

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