stabilizer_finset_singleton

Mathlib.Algebra.Pointwise.Stabilizer

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

English

The stabilizer of a singleton Finset equals the stabilizer of the element.

Русский

Стабилизатор одиночного финсета равен стабилизатору элемента.

LaTeX

$$$ \operatorname{Stabilizer}_G({b} : \mathrm{Finset} \alpha) = \operatorname{Stabilizer}_G b $$$

Lean4

@[to_additive (attr := simp)]
theorem stabilizer_finset_singleton (b : α) : stabilizer G ({ b } : Finset α) = stabilizer G b := by ext; simp

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

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

Разделы

Аффилиация

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