eq_of_zero_eq_one

Mathlib.Algebra.GroupWithZero.Basic

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

English

0 equals 1 implies all elements are equal.

Русский

0 равняется 1, следовательно все элементы равны.

LaTeX

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

Lean4

theorem eq_of_zero_eq_one (h : (0 : M₀) = 1) (a b : M₀) : a = b :=
  @Subsingleton.elim _ (subsingleton_of_zero_eq_one h) a b

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

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

Разделы

Аффилиация

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