eq_zero_or_unit

Mathlib.Algebra.GroupWithZero.Units.Basic

URI: https://scilib.ai/kg/mathlib#GroupWithZero.eq_zero_or_unit

English

In a group with zero, every element is either zero or a unit.

Русский

В группе с нулём каждый элемент либо ноль, либо единица (является единицей).

LaTeX

$$$\forall a:\ G_0,\ a=0 \\lor \\ \exists u:\ G_0^\times,\ a=u$$$

Lean4

theorem _root_.GroupWithZero.eq_zero_or_unit (a : G₀) : a = 0 ∨ ∃ u : G₀ˣ, a = u := by simpa using em _

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

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

Разделы

Аффилиация

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