smul_def

Mathlib.Algebra.Group.TransferInstance

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

English

The transported action is defined by r • x = e^{-1}( r • e x ).

Русский

Действие перенесено как r • x = e^{-1}( r • e x ).

LaTeX

$$$$r \cdot x = e^{-1}\big( r \cdot e x \big).$$$$

Lean4

@[to_additive]
theorem smul_def [SMul M β] (r : M) (x : α) :
    letI := e.smul M
    r • x = e.symm (r • e x) :=
  rfl

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

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

Разделы

Аффилиация

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