of_ne_one — Mathlib

English

No nontrivial element lies in the unit: for every m, m is not in 1.

Русский

Ни одно ненулевое слово не принадлежит единице: для любого m выполняется m ∉ 1.

LaTeX

$$$\\\\forall m, \\\\; m \\\\in (1 : FreeMonoid \\alpha) \\\\Rightarrow \\\\; \\\\text{False}$$$

Lean4

@[to_additive (attr := simp)]
theorem of_ne_one (a : α) : of a ≠ 1 := by
  intro h
  have := congrArg FreeMonoid.length h
  simp only [length_of, length_one, Nat.succ_ne_self] at this

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