zeroUnique

Mathlib.GroupTheory.Perm.Cycle.Type

URI: https://scilib.ai/kg/mathlib#Equiv.Perm.VectorsProdEqOne.zeroUnique

English

There is a unique 1-length vector in vectorsProdEqOne(G,1), namely the vector with entry 1.

Русский

Существует единственный вектор длины 1 с произведением 1: единичный элемент.

LaTeX

$$vectorsProdEqOne(G,1) = { Vector.nil.cons 1 }$$

Lean4

instance zeroUnique : Unique (vectorsProdEqOne G 0) :=
  by
  rw [zero_eq]
  exact Set.uniqueSingleton Vector.nil

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

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

Разделы

Аффилиация

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