zero_ne_one_or_forall_eq_0

Mathlib.Algebra.GroupWithZero.Basic

URI: https://scilib.ai/kg/mathlib#zero_ne_one_or_forall_eq_0

← MathLib Explorer

English

In a monoid with zero, either 0 ≠ 1 or every element equals 0.

Русский

В моноиде с нулём либо 0 ≠ 1, либо каждый элемент равен 0.

LaTeX

$$0 \neq 1 \lor \forall a, a = 0$$

Lean4

/-- In a monoid with zero, either zero and one are nonequal, or zero is the only element. -/
theorem zero_ne_one_or_forall_eq_0 : (0 : M₀) ≠ 1 ∨ ∀ a : M₀, a = 0 :=
  not_or_of_imp eq_zero_of_zero_eq_one

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

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

Разделы

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

Аффилиация

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