univ

Mathlib.Data.Fintype.Units

URI: https://scilib.ai/kg/mathlib#UnitsInt.univ

English

The universe of the unit group of integers is exactly {1, -1}.

Русский

Обозначение унивита для группы единиц целых равно {1, -1}.

LaTeX

$$$$(\\mathrm{univ}_{\\mathbb{Z}^{\\times}}) = \\{1, -1\\}.$$$$

Lean4

@[simp]
theorem univ : (Finset.univ : Finset ℤˣ) = {1, -1} :=
  rfl

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

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

Разделы

Аффилиация

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