Product — Mathlib

English

The finite product of Dihedral groups indexed by a list l is the direct product over i : Fin(l.length) of DihedralGroup(l[i]).

Русский

Конечное произведение диагедральных групп, индексируемое списком l, есть прямое произведение по индексам i : Fin(l.length) из групп DihedralGroup(l[i]).

LaTeX

$$$ \text{Product}(l) = \prod_{i=0}^{|l|-1} \mathrm{DihedralGroup}(l_i). $$$

Lean4

/-- A finite product of Dihedral groups. -/
abbrev Product (l : List ℕ) : Type :=
  ∀ i : Fin l.length, DihedralGroup l[i]

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