stabilizer_finset_empty

Mathlib.Algebra.Pointwise.Stabilizer

URI: https://scilib.ai/kg/mathlib#MulAction.stabilizer_finset_empty

← MathLib Explorer

English

The stabilizer of the empty finite set is the whole group.

Русский

Стабилизатор пустого конечного множества равен всей группе.

LaTeX

$$$ \operatorname{stabilizer}_G(\emptyset) = \top $$$

Lean4

@[to_additive (attr := simp)]
theorem stabilizer_finset_empty : stabilizer G (∅ : Finset α) = ⊤ :=
  Subgroup.coe_eq_univ.1 <| eq_univ_of_forall Finset.smul_finset_empty

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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