fintype

Mathlib.Data.Fintype.Units

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

English

The group of units of the integers consists of exactly two elements: ±1.

Русский

Группа единиц целых состоит ровно из двух элементов: ±1.

LaTeX

$$$$\\mathbb{Z}^{\\times} = \\{1, -1\\}.$$$$

Lean4

instance fintype : Fintype ℤˣ :=
  ⟨{1, -1}, fun x ↦ by cases Int.units_eq_one_or x <;> simp [*]⟩

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

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

Разделы

Аффилиация

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