isCyclicallyReduced_iff — Mathlib

English

IsCyclicallyReduced L is equivalent to IsReduced L together with a compatibility condition for the first and last letters: If a is the last letter and b is the first, then a and b agree on both symbol and sign.

Русский

Циклически сокращенное слово L эквивалентно тому, что L сокращено и выполняется совместимость первой и последней буквы: если a — последняя, а b — первая, то a и b совпадают по символу и знаку.

LaTeX

$$$$ \\mathrm{IsCyclicallyReduced}(L) \\iff \\mathrm{IsReduced}(L) \\land \\forall a \\in L.getLast?, \\forall b \\in L.head?, a.1 = b.1 \\rightarrow a.2 = b.2. $$$$

Lean4

@[to_additive]
theorem isCyclicallyReduced_iff :
    IsCyclicallyReduced L ↔ IsReduced L ∧ ∀ a ∈ L.getLast?, ∀ b ∈ L.head?, a.1 = b.1 → a.2 = b.2 :=
  Iff.rfl

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