isReduced_iff_reduce_eq

Mathlib.GroupTheory.FreeGroup.Reduce

URI: https://scilib.ai/kg/mathlib#FreeGroup.isReduced_iff_reduce_eq

English

IsReduced L is equivalent to reduce L = L.

Русский

IsReduced L эквивалентно reduce L = L.

LaTeX

$$$IsReduced L \iff reduce L = L$$$

Lean4

@[to_additive]
theorem isReduced_iff_reduce_eq : IsReduced L ↔ reduce L = L
    where
  mp h := h.reduce_eq
  mpr := .of_reduce_eq

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru