isCyclic_of_subsingleton — Mathlib

English

A group with a single element (subsingleton) is cyclic.

Русский

Группа, состоящая из одного элемента (subsingleton), циклична.

LaTeX

$$$$\\text{If } \\text{Subsingleton}(\\alpha) \\text{ and } G \\text{ is a group on } \\alpha, \\text{ then } \\operatorname{IsCyclic}(\\alpha).$$$$

Lean4

@[to_additive]
instance (priority := 100) isCyclic_of_subsingleton [Group α] [Subsingleton α] : IsCyclic α :=
  ⟨⟨1, fun _ => ⟨0, Subsingleton.elim _ _⟩⟩⟩

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