instIsScalarTower

Mathlib.Algebra.Ring.CentroidHom

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

English

If f' equals f, then the copy of f with target f' is equal to f.

Русский

Если f' равно f, то копия f с целевым отображением f' равна f.

LaTeX

$$copy_eq (f : CentroidHom α) (f' : α → α) (h : f' = f) : f.copy f' h = f$$

Lean4

instance [SMul M N] [IsScalarTower M N α] : IsScalarTower M N (CentroidHom α) where
  smul_assoc _ _ _ := ext fun _ => smul_assoc _ _ _

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

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

Разделы

Аффилиация

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