one_ne_of — Mathlib

English

Let α be a type. The unit element 1 of the free ring is not the image of any generator; i.e., 1 ≠ of x for all x ∈ α.

Русский

Пусть α — тип. Единица набора свободного кольца не является образoм порождающего: для любого x из α верно 1 ≠ of x.

LaTeX

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

Lean4

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

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