of

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.prod.of

English

If g : FreeGroup α →* α satisfies ∀ x, g (FreeGroup.of x) = x, then ∀ x, g x = prod x.

Русский

Если g : FreeGroup α →* α удовлетворяет ∀ x, g(of x) = x, тогда ∀ x, g x = prod x.

LaTeX

$$$ \\forall g:\\mathrm{FreeGroup}\\ α \\to^* α,\\; (\\forall x, g(\\mathrm{FreeGroup.of} x) = x) \\Rightarrow \\forall x, g x = prod x $$$

Lean4

@[to_additive (attr := simp)]
theorem of {x : α} : prod (of x) = x :=
  lift_apply_of

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

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

Разделы

Аффилиация

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