one_ne_of — Mathlib

English

The unit element 1 of the monoid is not equal to the image of any generator under the canonical embedding of α into FreeMonoid α.

Русский

Единица 1 моноида не равна изображению какого-либо генератора через каноническое внедрение α в FreeMonoid α.

LaTeX

$$$$1 \neq \operatorname{of}(a) \quad\text{for all } a \in \alpha.$$$$

Lean4

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

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