isReduced_toWord — Mathlib

English

Let α be a type. For every x in the free group on α, the word x.toWord is reduced.

Русский

Пусть α — множество. Для каждого элемента x свободной группы на α выполняется, что x.toWord является редуцированным словом.

LaTeX

$$$$\\\\forall {\\\\alpha} \\, (x: FreeGroup(\\\\alpha)), IsReduced(x.toWord).$$$$

Lean4

@[to_additive]
theorem isReduced_toWord {x : FreeGroup α} : IsReduced x.toWord := by simp [isReduced_iff_reduce_eq]

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