coe_pointwise_smul

Mathlib.Algebra.Group.Subgroup.Pointwise

URI: https://scilib.ai/kg/mathlib#Subgroup.coe_pointwise_smul

English

For a, G, S, the set-theoretic image of a • S equals a acting on the set S: ↑(a • S) = a • (S : Set G).

Русский

Для a, S: ↑(a • S) = a • (S : Set G).

LaTeX

$$$\\uparrow(a\\cdot S) = a\\cdot (S:\\mathrm{Set}~G)$$$

Lean4

@[simp, norm_cast]
theorem coe_pointwise_smul (a : α) (S : Subgroup G) : ↑(a • S) = a • (S : Set G) :=
  rfl

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

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

Разделы

Аффилиация

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