map_mul

Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs

URI: https://scilib.ai/kg/mathlib#Matrix.GeneralLinearGroup.map_mul

English

The map respects multiplication: map f (g h) = map f g · map f h.

Русский

Отображение сохраняет умножение: map f (g h) = map f g · map f h.

LaTeX

$$\\mathrm{map}\\,f\\ (g h) = (\\mathrm{map}\\,f\\,g) \\cdot (\\mathrm{map}\\,f\\,h)$$

Lean4

protected theorem map_mul (g h : GL n R) : map f (g * h) = map f g * map f h := by simp only [map_mul]

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

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

Разделы

Аффилиация

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