vectorsProdEqOne — Mathlib

English

The set of length-n vectors with entries in G whose product equals 1.

Русский

Множество векторов длины n над группой G, произведение которых равно единице.

LaTeX

$$$\\mathrm{vectorsProdEqOne}(G,n) = \\{ v \\in \\mathrm{List.Vector}\,G\\,n \\mid v.toList.prod = 1 \\}$$$

Lean4

/-- The type of vectors with terms from `G`, length `n`, and product equal to `1:G`. -/
def vectorsProdEqOne : Set (List.Vector G n) :=
  {v | v.toList.prod = 1}

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