subsingleton

Mathlib.Algebra.GroupWithZero.Regular

URI: https://scilib.ai/kg/mathlib#IsRegular.subsingleton

← MathLib Explorer

English

If 0 is regular, the ring is trivial (subsingleton).

Русский

Если 0 регулярен, кольцо тривиально.

LaTeX

$$IsRegular 0 → Subsingleton R$$

Lean4

/-- The element `0` is regular if and only if `R` is trivial. -/
theorem subsingleton (h : IsRegular (0 : R)) : Subsingleton R :=
  h.left.subsingleton

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

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

Разделы

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

Аффилиация

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