mk — Mathlib · SciLib

English

There is a canonical map mk from lists of pairs to the free group on α.

Русский

Существует каноническое отображение mk от списков пар в свободную группу на α.

LaTeX

$$$\mathrm{mk}: \mathsf{List}(\alpha \times \mathsf{Bool}) \to \mathrm{FreeGroup}(\alpha).$$$

Lean4

/-- The canonical map from `List (α × Bool)` to the free group on `α`. -/
@[to_additive /-- The canonical map from `List (α × Bool)` to the free additive group on `α`. -/
    ]
def mk (L : List (α × Bool)) : FreeGroup α :=
  Quot.mk Red.Step L

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