norm — Mathlib

English

The norm on FreeGroup α is given by the length of the reduced word: norm(x) = |x.toWord|.

Русский

Норма на свободной группе над α равна длине редуцированного слова: norm(x) = |x.toWord|.

LaTeX

$$$$\\forall {\\\\alpha} \\, [\\\\text{DecidableEq }\\\\alpha],\\\\; \\forall x: FreeGroup(\\\\alpha),\\\\; \\mathrm{norm}(x) = |x.toWord|.$$$$

Lean4

/-- The length of reduced words provides a norm on a free group. -/
@[to_additive /-- The length of reduced words provides a norm on an additive free group. -/
    ]
def norm (x : FreeGroup α) : ℕ :=
  x.toWord.length

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