ofGroup — Mathlib

English

The NormalWord corresponding to a group element g ∈ G is the simple word whose head is g and which has no letters in its tail.

Русский

NormalWord, соответствующее элементу g ∈ G, — это простое слово, голова которого равна g, а хвост пуст.

LaTeX

$$$\\mathrm{ofGroup}(g) : \\text{NormalWord } d$ defined by head := g, toList := []$$

Lean4

/-- The `NormalWord` representing an element `g` of the group `G`, which is just the element `g`
itself. -/
@[simps]
def ofGroup (g : G) : NormalWord d :=
  { head := g
    toList := []
    mem_set := by simp
    chain := List.isChain_nil }

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