red_iff_eq

Mathlib.GroupTheory.FreeGroup.Basic

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

English

If L1 is reduced, then Red(L1,L2) holds exactly when L2 = L1.

Русский

Если L1 редуцировано, то Red(L1,L2) верно тогда и только тогда, когда L2 = L1.

LaTeX

$$$\operatorname{IsReduced}(L_1) \rightarrow \big( \operatorname{Red}(L_1,L_2) \leftrightarrow L_2 = L_1 \big).$$$

Lean4

@[to_additive]
theorem red_iff_eq (h : IsReduced L₁) : Red L₁ L₂ ↔ L₂ = L₁ :=
  Relation.reflTransGen_iff_eq fun _ => h.not_step

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

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

Разделы

Аффилиация

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