instSMul

Mathlib.Algebra.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.instSMul

English

If S acts on R, then there is a natural SMul S ℍ(R), i.e., ℍ(R) is an S-module.

Русский

Если S действует на R, то ℍ(R) естественно является модулем над S.

LaTeX

$$$$ \mathbb{H}(R) \text{ carries an } S\text{-module structure whenever } S \text{ acts on } R. $$$$

Lean4

instance [SMul S R] : SMul S ℍ[R] :=
  inferInstanceAs <| SMul S ℍ[R,-1,0,-1]

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

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

Разделы

Аффилиация

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