eq_one

Mathlib.Algebra.Notation.Defs

URI: https://scilib.ai/kg/mathlib#Subsingleton.eq_one

English

If a type has One and is a Subsingleton, then every element equals 1.

Русский

Если у типа есть единица и он является подсчётной однородной структурой, то любой элемент равен 1.

LaTeX

$$$$\\forall a \\in \\alpha,\\ a = 1.$$$$

Lean4

@[to_additive]
theorem eq_one [One α] [Subsingleton α] (a : α) : a = 1 :=
  Subsingleton.elim _ _

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

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

Разделы

Аффилиация

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