instNonemptyElemCommutatorSet

Mathlib.GroupTheory.Commutator.Basic

URI: https://scilib.ai/kg/mathlib#instNonemptyElemCommutatorSet

English

The commutatorSet G is nonempty (it contains at least the identity, hence at least one element of G).

Русский

Mножество commutatorSet(G) непусто (оно содержит по крайней мере единицу, следовательно, как минимум один элемент G).

LaTeX

$$Nonempty (commutatorSet G)$$

Lean4

instance : Nonempty (commutatorSet G) :=
  ⟨⟨1, one_mem_commutatorSet G⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru