of_ne_one

Mathlib.GroupTheory.FreeGroup.Reduce

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

English

For every a in α, the image of a under the canonical embedding into the free group is not the identity.

Русский

Пусть a принадлежит α. Образ a в свободной группе над α не является единицей.

LaTeX

$$$$\\forall a: \\alpha, of(a) \\neq 1.$$$$

Lean4

@[to_additive (attr := simp)]
theorem of_ne_one (a : α) : of a ≠ 1 :=
  one_ne_of _ |>.symm

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

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

Разделы

Аффилиация

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