subsingleton_iff_zero_eq_one

Mathlib.Algebra.GroupWithZero.Basic

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

← MathLib Explorer

English

If a*b ≠ 0, then b ≠ 0.

Русский

Если a·b ≠ 0, то b ≠ 0.

LaTeX

$$a \cdot b \neq 0 \rightarrow b \neq 0$$

Lean4

/-- In a monoid with zero, zero equals one if and only if all elements of that semiring
are equal. -/
theorem subsingleton_iff_zero_eq_one : (0 : M₀) = 1 ↔ Subsingleton M₀ :=
  ⟨fun h =>
    haveI := uniqueOfZeroEqOne h;
    inferInstance,
    fun h => @Subsingleton.elim _ h _ _⟩

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

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

Разделы

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

Аффилиация

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