eq_zero_of_zero_eq_one

Mathlib.Algebra.GroupWithZero.Basic

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

← MathLib Explorer

English

If 0 = 1 in a MonoidWithZero, then every element equals 0.

Русский

Если 0 = 1 в MonoidWithZero, то каждый элемент равен 0.

LaTeX

$$0 = 1 \rightarrow \forall a, a = 0$$

Lean4

/-- In a monoid with zero, if zero equals one, then zero is the only element. -/
theorem eq_zero_of_zero_eq_one (h : (0 : M₀) = 1) (a : M₀) : a = 0 := by rw [← mul_one a, ← h, mul_zero]

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

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

Разделы

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

Аффилиация

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