of_ne_one — Mathlib

English

Let α be a type. For every x ∈ α the image of x under the canonical map to the free ring is not equal to 1; i.e., the generator is never identified with the multiplicative unit.

Русский

Пусть α — тип. Для каждого x ∈ α образ x в свободном кольце не равен единице; порождающий не отображается в единицу.

LaTeX

$$$$\forall x:\\alpha,\\ of$x$ \neq 1.$$$$

Lean4

@[simp]
theorem of_ne_one (x : α) : of x ≠ 1 :=
  FreeAbelianGroup.of_injective.ne <| FreeMonoid.of_ne_one _

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