of_subsingleton — Mathlib

English

If M is a singleton monoid, then for any x ∈ M, IsPrimitiveRoot x 1 holds.

Русский

Если имеется одиночное моноидное множество M, то для любого элемента x ∈ M выполняется IsPrimitiveRoot x 1.

LaTeX

$$$[Subsingleton\ M] \Rightarrow IsPrimitiveRoot(x,1)$$$

Lean4

@[nontriviality]
theorem of_subsingleton [Subsingleton M] (x : M) : IsPrimitiveRoot x 1 :=
  ⟨Subsingleton.elim _ _, fun _ _ ↦ one_dvd _⟩

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