stabilizer_coe_finset

Mathlib.Algebra.Pointwise.Stabilizer

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

← MathLib Explorer

English

Equality of stabilizers when translating Finset to Set.

Русский

Равенство стабилизаторов при преобразовании финсет к множеству.

LaTeX

$$$ \operatorname{Stabilizer}_G( s : Set \alpha) = \operatorname{Stabilizer}_G s $$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem stabilizer_coe_finset (s : Finset α) : stabilizer G (s : Set α) = stabilizer G s := by ext;
  simp [← Finset.coe_inj]

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

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

Разделы

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

Аффилиация

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