isScalarTower

Mathlib.GroupTheory.GroupAction.SubMulAction

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

English

The subtype p inherits a scalar tower: smul_assoc on p matches the tower smul on its elements.

Русский

Подтип p наследует скалярную башню: smul_assoc на p совпадает с башней smul на его элементах.

LaTeX

$$$IsScalarTower S R p$ with smul_assoc$$

Lean4

@[to_additive]
instance isScalarTower : IsScalarTower S R p where smul_assoc s r x := Subtype.ext <| smul_assoc s r (x : M)

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

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

Разделы

Аффилиация

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