smul_def

Mathlib.Algebra.Group.Subgroup.Actions

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

English

For g ∈ S ⊆ G and m ∈ α, the action of g on m in S agrees with the action of g viewed as an element of G on m: g • m = (g : G) • m.

Русский

Пусть g ∈ S ⊆ G и m ∈ α. Тогда действие g на m в S совпадает с действием g как элемента G на m: g • m = (g : G) • m.

LaTeX

$$$g \cdot m = (g : G) \cdot m$$$

Lean4

@[to_additive]
theorem smul_def (g : S) (m : α) : g • m = (g : G) • m :=
  rfl

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

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

Разделы

Аффилиация

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