instSMulMemClass

Mathlib.GroupTheory.GroupAction.SubMulAction

URI: https://scilib.ai/kg/mathlib#SubMulAction.instSMulMemClass

English

There is a SmulMemClass instance for SubMulAction R M by transporting the membership via the subtype.

Русский

Существует инстанс SMulMemClass для SubMulAction R M, получаемый через принадлежность к подтипу.

LaTeX

$$$SMulMemClass (SubMulAction R M) R M$$$

Lean4

@[to_additive]
instance : SMulMemClass (SubMulAction R M) R M where smul_mem := smul_mem' _

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

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

Разделы

Аффилиация

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