instSMulSubtypeMemSubmonoid

Mathlib.Algebra.Star.Unitary

URI: https://scilib.ai/kg/mathlib#unitary.instSMulSubtypeMemSubmonoid

English

There exists a canonical action of unitary(R) on unitary(A), making unitary(A) a module over unitary(R).

Русский

Существует каноническое действие единиц u(R) на единицах u(A), что делает u(A) модулем над u(R).

LaTeX

$$$\\text{MulAction}(\\mathrm{unitary}(R), \\mathrm{unitary}(A))$$$

Lean4

instance : SMul (unitary R) (unitary A) where smul r a := ⟨r • a, smul_mem r a.prop⟩

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

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

Разделы

Аффилиация

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