baseChange_pow

Mathlib.LinearAlgebra.TensorProduct.Tower

URI: https://scilib.ai/kg/mathlib#LinearMap.baseChange_pow

English

For endomorphisms f,g of M, baseChange_A(f g) equals baseChange_A(f) baseChange_A(g).

Русский

Для эндоморфизмов f,g модуля M, baseChange_A(f g) = baseChange_A(f) baseChange_A(g).

LaTeX

$$$$\\mathrm{baseChange}_A(f g)=(\\mathrm{baseChange}_A f)(\\mathrm{baseChange}_A g).$$$$

Lean4

theorem baseChange_pow (f : Module.End R M) (n : ℕ) : (f ^ n).baseChange A = f.baseChange A ^ n :=
  map_pow (Module.End.baseChangeHom _ _ _) f n

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

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

Разделы

Аффилиация

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