instIsScalarTower_1

Mathlib.Algebra.Ring.CentroidHom

URI: https://scilib.ai/kg/mathlib#CentroidHom.instIsScalarTower_1

English

There is a canonical homomorphism from the center of α into the center of the centroid: z ↦ (a ↦ z a).

Русский

Существует канонический гомоморфизм из центра α в центр центроидов: z ↦ (a ↦ z a).

LaTeX

$$$ center(\alpha) \toCentroidHom(\alpha) $ and the action is (a \mapsto z a)$$

Lean4

instance : IsScalarTower (CentroidHom α) α α where smul_assoc _ _ _ := (map_mul_right _ _ _).symm

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

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

Разделы

Аффилиация

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