instSProd — Mathlib

English

An instance provides the product of two lists as a list of pairs: List.product.

Русский

Экземпляр устанавливает произведение двух списков как список пар: List.product.

LaTeX

$$$\\mathrm{instSProd} : SProd(\\mathrm{List}\\,\\alpha)(\\mathrm{List}\\,\\beta)(\\mathrm{List}(\\alpha \\times \\beta))$ where $sprod$ is defined as $\\mathrm{List.product}$$$

Lean4

/-- Notation for calculating the product of a `List` -/
instance instSProd : SProd (List α) (List β) (List (α × β)) where sprod := List.product

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