instIsScalarTower

Mathlib.Algebra.Module.PUnit

URI: https://scilib.ai/kg/mathlib#PUnit.instIsScalarTower

English

There is IsScalarTower PUnit R S, i.e., the two-step scalar action via R and S is coherent on PUnit.

Русский

Существует IsScalarTower PUnit R S, то есть конгруэнтность последовательного скалярного действия через R и S на PUnit.

LaTeX

$$$\\text{IsScalarTower } PUnit\\; R\\; S.$$$

Lean4

instance [SMul R S] : IsScalarTower PUnit R S :=
  ⟨by simp⟩

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

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

Разделы

Аффилиация

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