reduce_eq

Mathlib.GroupTheory.FreeGroup.Reduce

URI: https://scilib.ai/kg/mathlib#FreeGroup.IsReduced.reduce_eq

English

If L is reduced, then reducing L yields L itself.

Русский

Если L редуцирован, то редукция L даёт сам L.

LaTeX

$$$\forall h : IsReduced L ,\; reduce L = L$$$

Lean4

@[to_additive]
theorem reduce_eq (h : IsReduced L) : reduce L = L :=
  by
  rw [← h.red_iff_eq]
  exact reduce.red

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

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

Разделы

Аффилиация

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