zero

Mathlib.Algebra.Regular.SMul

URI: https://scilib.ai/kg/mathlib#IsSMulRegular.zero

← MathLib Explorer

English

The statement that 0 is M-regular is equivalent to M being a Subsingleton.

Русский

Тождество о том, что 0 является M-регулярным, эквивалентно тому, что M является субодиночным.

LaTeX

$$$IsSMulRegular M 0 \iff Subsingleton M$$$

Lean4

/-- The element `0` is `M`-regular when `M` is trivial. -/
theorem zero [sM : Subsingleton M] : IsSMulRegular M (0 : R) :=
  zero_iff_subsingleton.mpr sM

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

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

Разделы

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

Аффилиация

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