instNontrivialOfNonempty — Mathlib

English

If α is nonempty, then the free group on α is nontrivial (has two distinct elements).

Русский

Если α непусто, тогда свободная группа на α нетривиальна (существуют два различных элемента).

LaTeX

$$$$\\forall {\\\\alpha} \\, [\\\\text{Nonempty }\\\\alpha],\\\\; Nontrivial(FreeGroup(\\\\alpha)).$$$$

Lean4

@[to_additive]
instance [Nonempty α] : Nontrivial (FreeGroup α) where
  exists_pair_ne :=
    let ⟨x⟩ := ‹Nonempty α›;
    ⟨1, of x, one_ne_of x⟩

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