one_ne_of — Mathlib

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, 1 \\neq of(a).$$$$

Lean4

@[to_additive (attr := simp)]
theorem one_ne_of (a : α) : 1 ≠ of a :=
  letI := Classical.decEq α;
  ne_of_apply_ne toWord <| by simp

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