stabilizer_finset_univ

Mathlib.Algebra.Pointwise.Stabilizer

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

English

The stabilizer of the universal Finset is the top subgroup.

Русский

Стабилизатор универсльного финсета равен верхнему подгруппе.

LaTeX

$$$ \operatorname{stabilizer}_G(\mathrm{Finset.univ}) = \top $$$

Lean4

@[to_additive (attr := simp)]
theorem stabilizer_finset_univ [Fintype α] : stabilizer G (Finset.univ : Finset α) = ⊤ :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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