Reduced — Mathlib

English

A word in CoprodI is reduced if none of its letters lie in the image of the base group; i.e., no letter g at position t belongs to (φ t).range.

Русский

Слово в CoprodI сокращено, если ни одна буква не лежит в образе базовой группы; никакая буква g на позиции t не принадлежит (φ t).range.

LaTeX

$$$$\mathrm{Reduced}(φ, w) \iff \forall g,\; g \in w.toList \Rightarrow g.2 \notin (φ g.1).range.$$$$

Lean4

/-- A word in `CoprodI` is reduced if none of its letters are in the base group. -/
def Reduced (w : Word G) : Prop :=
  ∀ g, g ∈ w.toList → g.2 ∉ (φ g.1).range

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