subgroup_smul_def

Mathlib.GroupTheory.GroupAction.Defs

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

English

For H ≤ G, a ∈ H, b ∈ α, the action a • b equals (a : G) • b.

Русский

Для a ∈ H, b ∈ α, действие a • b равно (a : G) • b.

LaTeX

$$$$ a \\cdot b = (a : G) \\cdot b. $$$$

Lean4

@[to_additive]
theorem subgroup_smul_def {H : Subgroup G} (a : H) (b : α) : a • b = (a : G) • b :=
  rfl

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

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

Разделы

Аффилиация

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