coe_smul

Mathlib.GroupTheory.GroupAction.Defs

URI: https://scilib.ai/kg/mathlib#MulAction.orbitRel.Quotient.orbit.coe_smul

English

The scalar action on an orbit element is the same as the underlying action on α after coercion.

Русский

Действие на элементе орбиты через приведённое отображение совпадает с действием на α.

LaTeX

$$$↑(g \cdot a) = g \cdot (a : α)$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_smul {g : G} {x : orbitRel.Quotient G α} {a : x.orbit} : ↑(g • a) = g • (a : α) :=
  rfl

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

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

Разделы

Аффилиация

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